Paradigmatic examples of MMT content. They are used for development and regression testing.

The Meta Information for the ODK Group.

The knowledge for integrating the Sage system into the OpenDreamKit virtual Research Environment.

The knowledge for integrating the GAP system into the OpenDreamKit virtual Research Environment.

The library of the MathScheme project. See http://www.cas.mcmaster.ca/research/mathscheme/

The Logic Atlas and Integrator project content (still in TWELF, not MMT syntax)

The Theories for the LMFDB data base.

The general mathematical knowledge needed for the OpenDreamKit Virtual Research Environment.

Examples from the course Knowledge Representation for Mathematical Theories (https://kwarc.info/courses/KRMT/) given by Kohlhase and Rabe at University Erlangen-Nuremberg in Summer 2020.

The Knowledge behind the FindStat project

The Formalizations for the UFrameIT-based serious game FrameWorld.

OMDoc/MMT Tutorial for Mathematicians