This package contains a few sample databases for the Metamath language. You can read them and discover the proof they bring, or you can add your own proofs of other mathematical statements. Check out in particular the file set.mm, which contain many modern mathematical results proved al the way from the axioms of set theory. A graphical and interactively browsable rendition of the same database is available as the Metamath Proof Explorer[1]. [1] http://us.metamath.org/mpeuni/mmset.html You can check the correctness of a Metamath database using the metamath program (contained in the metamath package). For example, to check that the file set.mm is correct you can use: $ metamath 'read "/usr/share/metamath/databases/set.mm"' 'verify proof *' 'exit' Using the same program you can edit the proofs or add new theorems and their proofs. Please check out the book "Metamath, A Computer Language for Pure Mathematics"[2], by Norman Megill, for more information on how to use the program and on the Metamath language itself. [2] http://us.metamath.org/downloads/metamath.pdf See also the Metamath website[3] to learn more about Metamath and its community. If you'd like to contribute your proofs to the Metamath project, please read the file CONTRIBUTING.md and get in touch with the community. [3] http://us.metamath.org/