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

These archives can be installed and managed using lmh functionality provided by MMT.