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:

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