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 71 proofs proven by Metamath from this list of 100. As of 2019-03-10 this number of proofs is more than Coq (69), Mizar (69), ProofPower (43), nqthm/ACL2 (18), PVS (16), and NuPRL/MetaPRL (8); it is short of only Isabelle (81) 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. In this page, you can see the completed Metamath proofs and the Metamath proofs to be done from this list of metamath proofs. Some graphs showing Metamath 100 progress are available (click the Authors tab for a pie chart).

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. 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 a dozen independently-written verifiers) is very stable over time.

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.)

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 email missing entries to Norm Megill! The intuitionistic logic explorer (iset.mm) database also includes finds and findes.

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 released via a GitHub pull request and will later be moved to the main part of set.mm by its maintainers as appropriate. Alternately, mathboxes can be emailed to Norm. Requests for help on the Metamath Google Group 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