The MMT Language and System

Flexiformal Knowledge

Currently, MMT concentrates on the formal subset of the OMDoc, which postulates that mathematatical knowledge should be represented flexiformally, i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in Mihnea Iancu’s PhD thesis. The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet.

The bulk of flexiformalizations in the MMT world are generated from sTeX, a semantics-enhanced version of LaTeX which can be converted to flexiformal MMT. Much of this content is hosted on MathHub.