Explore projects

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

The Knowledge behind the FindStat project

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

The Meta Information for the ODK Group.

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

Metalogical frameworks that extend LF - the Edinburgh Logical Framework. These provide common features - e.g. record types, subtyping, or flexary functions - of logical languages at the meta-level for inheritance in LFX-specified logics.

The Theories for the LMFDB data base.

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

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

The Formalizations for the UFrameIT-based serious game FrameWorld.

OMDoc/MMT Tutorial for Mathematicians