MMTTeX: Connecting Content and Narration-Oriented Document Formats

摘要

Narrative, presentation-oriented assistant systems for mathematics such as LATEX 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 LATEX for the narrative and Mmt for the content-oriented representation. Formal objects may be written in MMT and imported into LATEX documents or written in the LATEX document directly. In the latter case, Mmt parses and checks the formal content during LATEX compilation and substitutes it with LATEX presentation macros. Besides checking the formal objects, this allows generating higher-quality LATEX 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.