Metamath
| Metamath | |
|---|---|
| Developer(s) | Norman Megill |
| Initial release | 0.07 in June 2005 |
| Stable release | 0.198
/ 7 August 2021 |
| Repository | |
| Written in | ANSI C |
| Operating system | Linux, Windows, macOS |
| Type | Computer-assisted proof checking |
| License | GNU General Public License (Creative Commons Public Domain Dedication for databases) |
| Website | us |
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.