MathHub Surface Formats

Flexiformal content in MathHub can be authored in various surface formats better suited for human manipulation.

MathHub currently supports the following five surface formats natively:

• HTML5 and TeX/LaTeX (as a minimally flexiformal document formats)
• sTeX (semantic TeX/LaTeX) is an extension of LaTeX that allows to annotate LaTeX documents with semantic properties and relations.
• MMT syntax.
• TWELF (Edinburgh Logical Framework in TWELF syntax)

Additionally, the native formats of the theorem prover libraries imported into MathHub are handled by special importers on a system-by-system basis.

Flexiformal content authored in any of these surface formats can is converted to OMDoc/MMT format for interoperability and processing in MathHub.info.