The MMT Language and System

The Open Archive of Formalizations (OAF)

The OAF is a repository backend for mathematical content hosted at It is the main place to develop and publish MMT archives.


In particular, the OAF contains the following MMT archives:

archive contents depends on
MMT/urtheories various top level languages, in particular the logical framework LF  
MMT/examples an example archive for beginners MMT/urtheories
MMT/experimental similar to MMT/examples but not always working MMT/urtheories
MMT/LATIN the LATIN logic atlas MMT/urtheories
MMT/LFX (experimental) various LF extensions and modifications, e.g. subtyping, record types and HOTT MMT/urtheories
Mizar/mml the Mizar Mathematical Library MMT/LATIN
TPTP/Distribution the TPTP problem library MMT/LATIN
HOLLight/basic the standard library of HOL Light MMT/LATIN


To work with the archives in the OAF, you usually want to clone the relevant git repositories and then add your local working copies to the math path. To clone the repositories, you typically proceed along the following lines:

mkdir content
cd content

mkdir MMT
cd MMT
git clone
git clone
git clone
cd ..

mkdir HOLLight
cd HOLLight
git clone
cd ..

mkdir Mizar
cd Mizar
git clone
cd ..

mkdir TPTP
git clone
cd .. 

You can also issue the clone command via MMT using the clone command of the shell. In that case, MMT automatically checks out all dependencies.