LaTeX Processing

MMT can serve as a LaTeX interpreter that turns LaTeX into MMT data structures for informal knowledge.

It consists if the following steps:

1. sTeX is used as a LaTeX style to mix formal with informal content
2. LaTeXML is used to process the LaTeX sources
3. the sTeX extension to MMT (see the project src/mmt-stex) interprets the LaTeXML output as MMT content
4. any MMT algorithms (e.g., HTML generation) are called on the MMT content

Much of this workflow in Mihnea Iancu’s PhD thesis. But it is already used heavily in Michael Kohlhase’s KWARC group for producing lecture materials.

Only partial documentation exists at this point:

• Integration with sTeX
• Integration with LaTeXML