Metamath
Sign in to saveAlso known as Metamath Proof Explorer, metamath.org
Metamath is a formal language and an associated computer program (a proof assistant) for archiving and verifying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.
Wikidata facts
- Official website
- metamath.org
Show 4 more facts
- Alexa rank
- 2394814
- source code repository URL
- github.com/metamath/set.mm
- software version identifier
- 0.06b
- Stack Exchange tag
- proofassistants.stackexchange.com/tags/metamath
via Wikidata · CC0
~13 min read
Article
19 sectionsContents
- Metamath language
- Language basics
- Proofs
- Substitution
- Metamath proof checker
- Metamath databases
- Metamath Proof Explorer
- Intuitionistic Logic Explorer
- New Foundations Explorer
- Higher-Order Logic Explorer
- Databases without explorers
- Older explorers
- Natural deduction
- Other works connected to Metamath
- Proof checkers
- Editors
- See also
- References
- External links
Metamath is a formal language and an associated computer program (a proof assistant) for archiving and verifying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.
By 2023, Metamath had been used to prove 74 of the 100 theorems of the "Formalizing 100 Theorems" challenge. At least 19 proof verifiers use the Metamath format. The Metamath website provides a database of formalized theorems which can be browsed interactively.