Package: metamath-databases (0.0.0~20210101.git55fe226-2)

Sample databases for Metamath

Metamath is a tiny language for expressing theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.

This package contains a number of Metamath databases developed collectively by people from the Metamath project, including set.mm (Metamath Proof Explorer) and others available at http://us.metamath.org/.

You can edit and verify these databases with any tool implementing the Metamath language, including the reference implementation available in the package metamath.

This page is also available in the following languages (How to set the default document language):