MathHub.info groups content by user accounts and independent libraries, e.g. the libraries of theorem provers that are maintained by whole communities.
MathHub libraries consist of individual math archives that are individually versioned and carry individual sets of permissions.
- PVS Group
The library of the PVS theorem prover in OMDoc/MMT.
- SMGloM: The Semantic Multilingual Glossary for Mathematics
The SMGloM is a structured terminology for mathematics. It combines lexical information about the "Words of Mathematics" (in multiple languages) with semantic information about their dependencies. Multiple services can be derived from this terminology, e.g. a classical glossary and a math dictionary.
- TPS Group
TPS, the "Theorem Proving System" is the first automated theorem prover for simple type theory. Its library contains a collection of classic theorems proved by TPS.
- HOL Light
Archives written in and imported from the HOL Light system
- The Mizar Mathematical Library at MathHub.info
With more than 10.000 definitions and 50.000 Theorems, the Mizar Mathematical Library (OEIS) is one of the leading libraries of formalized mathematics. We export the library into OMDoc connect it to other libraries and add semantic services.
- OpenDreamKit System Ontologies
The archives of the OpenDreamKit EU Project, see http://opendreamkit.org
- Hello World Examples for MathHub.info
This Library contains various paradigmatic "Hello World" Examples for MathHub
- The Math-in-the-Middle Ontology
The Math-in-the-Middle Ontology is a curated theory-graph representation of mathematical knowledge that serves as an integrating ontology for mathematical software systems and services.
- MMT Core libraries built and maintained by the MMT group
- MiKoMH: Michael Kohlhase's Flexiformal Course Materials and Talks
The course materials (slides, course notes, problems, and exams of six courses) and scientific talks flexiformally preloaded in sTeX.
- SMGloM The Semantic Multilingual Glossary for Mathematics (External)