MMTTeX

MMTTeX: connecting content and narration-oriented document formats. Narrative, presentation-oriented assistant systems for mathematics such as Open image in new window on the one hand and formal, content-oriented ones such as proof assistants and computer algebra systems on the other hand have so far been developed and used largely independently. The former excel at communicating mathematical knowledge and the latter at certifying its correctness. MMTTeX aims at combining the advantages of the two paradigms. Concretely, we use Open image in new window for the narrative and Mmt for the content-oriented representation. Formal objects may be written in MMT and imported into Open image in new window documents or written in the Open image in new window document directly. In the latter case, Mmt parses and checks the formal content during Open image in new window compilation and substitutes it with Open image in new window presentation macros. Besides checking the formal objects, this allows generating higher-quality Open image in new window than could easily be produced by hand, e.g., by inserting hyperlinks and tooltips into formulas. Moreover, it allows reusing formalizations across narrative documents as well as between formal and narrative ones. As a case study, the present document was already written with MMTTeX.