Metamath 100  

Created by David A. Wheeler

"Formalizing 100 Theorems" by Freek Wiedijk lists 100 mathematical theorems and the various systems that have formalized a nontrivial number of them. This list is discussed in "Formal Proof - Getting Started" (Freek Wiedijk, Notices of the AMS, Volume 55, Number 11, December 2008). Rightly or wrongly, this list is used by others to judge proof systems. Wiedijk's "getting started" picks as its primary examples HOL Light and Mizar, which at the time had the largest number of proofs. Similarly, "Case Studies in Proof Checking" by Robert C. Kam says, "Judging by Dr. Wiedijk's Formalizing 100 Theorems list, which gives an overview of the headway various proof systems have made in mathematics, Coq and Mizar are two of the most successful systems in use today (Wiedijk, 2007)".

Currently there are 74 proofs proven by Metamath from this list of 100. As of 2020-04-05 this number of proofs is more than Coq (70), Mizar (69), ProofPower (43), Lean (29), PVS (22), nqthm/ACL2 (18), and NuPRL/MetaPRL (8); it is short of only Isabelle (83) and HOL Light (86). This is very good, especially considering that there had been no significant effort until 2014 to prove theorems from this list of 100 using Metamath. In this page, you can see the completed Metamath proofs and the Metamath proofs to be done from this list of metamath proofs.

Like all Metamath proofs, all reasoning is done directly in the proof itself rather than by algorithms embedded in the verification program. As a result, the proofs are completely transparent with nothing hidden from the user, and every step can be followed through a hyperlink to its corresponding proof or definition. Therefore, the Metamath Proof Explorer (MPE aka set.mm) database is the largest database of formally-verified mathematics that records every step of a proof by directly referring to only an axiom or previous proof (many competing databases only record tactics that are intended to rediscover the proof, instead of recording the specific proven steps actually used in the proof).

The theorems in MPE are routinely verified by 5 different programs written in 5 different programming languages by more than 5 different people. These are the original metamath (a C verifier by Norm Megill), mmj2 (a Java verifier by Mel O'Cat and Mario Carneiro), smetamath-rs (a high-speed Rust verifier by Stefan O'Rear), checkmm (a C++ verifier by Eric Schmidt), and mmverify (a Python verifier by Raph Levien). This checking by multiple independent verifiers in different languages provides very strong justification for believing that the proofs are correct.

What's more, all of the proofs listed here are current and verified with the current versions of Metamath tools. This is not the case with some other systems, where older proofs have not always been kept synchronized with the current system and thus have become essentially lost.

Since the kernel of Metamath is extremely small and rarely changes, the underlying Metamath language (as implemented by over a dozen independently-written verifiers) is very stable over time and can be verified very rapidly. The entire content of set.mm set theory database can be verified in less than 5 sec with the metamath program and in 0.7 sec with a recent version of Stefan O'Rear's smm3 verifier that utilizes multiple CPU cores. As of June 2016, altogether the theorems listed here ultimately make use of 12151 of the 28366 theorems in set.mm for their full derivation from ZFC axioms. (This doesn't mean that 12151 theorems are dedicated to the theorems on this list. Most are library-type theorems shared by many other theorems; for example, many of the theorems on this list depend on the complex number construction, which itself involves 3014 theorems to derive starting from the ZFC axioms.)

Some graphs showing Metamath 100 progress are available on another page (click the Authors tab for a pie chart). You can also see a Gource Visualization of the growth of the Metamath Proof Explorer (MPE / set.mm) database of proofs.

Here is the list of the Metamath proofs that are available from this list of 100, along with credit to the individual(s) who created the Metamath formalization. Almost all of these proofs are from the Metamath Proof Explorer, aka database set.mm, which is based on classical logic. However, there are some proofs available in the Intuitionistic Logic Explorer, aka database iset.mm, which uses intuitionistic logic instead. Please let us know about missing entries via github issue or the Metamath mailing list.

Note for potential contributors: The development tools most people use, in addition to a good text editor, are mmj2 (which has an introductory video) and the metamath program (which has a tutorial in Chapter 2 of the Metamath book). Most contributors keep their work in progress in private sections of set.mm called "mathboxes" to prevent interfering with others' work. Mathboxes can be updated via a GitHub pull request and will later be moved to the main part of set.mm as appropriate. Requests for help on the Metamath mailing list can help things go smoother. See the Most Recent Proofs page for recent announcements.

The page "Formalizing 100 Theorems" also contains a supplementary list of "obvious omissions" from the 100. Of those, the following have been formalized:

These are all the theorems from the list of 100 that have not been formalized in Metamath. Please move these to the above list!

You can see other proofs done with Metamath and for traditional mathematics on the Metamath Proof Explorer Home Page. Note that there are pages similar to this one for other tools, such as these pages on HOL and Mizar.

This metamath list was originally developed by David A. Wheeler and Norman Megill. If you add new theorems to the list, please tell Freek Wiedijk (freek at cs dot ru dot nl)

This page is dedicated to the public domain through the Creative Commons license CC0, to maximize the availability of this page's information.

W3C HTML validation