The OAF is a repository backend for mathematical content hosted at gl.mathhub.info.
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.