Databases
Metamath comes along with two main databases set.mm and ql.mm. set.mm stores theorems concerning ZFC theory and ql.mm develops a set of quantum logic theorems. Three internet interfaces (the Metamath Proof Explorer, the Hilbert Space Explorer and the Quantum Logic Explorer) are provided to explore these two databases in a human friendly way.
set.mm is by far the biggest database written for Metamath, but there is also a formalization (by Robert Solovay) of Peano arithmetic called peano.mm (included in metamath.zip) and a formalization of natural deduction called nat.mm. There is a database based on the formal system MIU presented in Gödel, Escher, Bach. Raph Levien has also designed several databases for his Ghilbert program.
Read more about this topic: Metamath