Metamath
Formal language and associated computer program / From Wikipedia, the free encyclopedia
Dear Wikiwand AI, let's keep it short by simply answering these key questions:
Can you list the top facts and stats about Metamath?
Summarize this article for a 10 year old
Metamath is a formal language and an associated computer program (a proof assistant) for archiving and verifying mathematical proofs.[2] 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.[3]
Developer(s) | Norman Megill |
---|---|
Initial release | 0.07 in June 2005; 18 years ago (2005-06) |
Stable release | |
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 | metamath |
As of September 2023[update], the set of proved theorems using Metamath includes 74[4] of the 100 theorems of the "Formalizing 100 Theorems" challenge,[5] making it fifth after Isabelle, HOL Light, Coq, and Lean. There are at least 19 proof verifiers that use the Metamath format.[6] The Metamath website provides a database of formalized theorems which can be browsed interactively.[7]