Metamath Home

Metamath 100

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

• 1. The Irrationality of the Square Root of 2 (sqrt2irr, by Norman Megill, 2001-08-20). The intuitionistic logic explorer (iset.mm) database also includes sqrt2irrap (by Jim Kingdon, 2022-02-01).
• 2. The Fundamental Theorem of Algebra (fta, by Mario Carneiro, 2014-09-15)
• 3. The Denumerability of the Rational Numbers (qnnen, by Norman Megill, 2004-07-31, revised by Mario Carneiro, 2013-03-03). The intuitionistic logic explorer (iset.mm) database also includes qnnen (by Jim Kingdon, 2023-08-11)
• 4. Pythagorean Theorem (cphpyth, by Norman Megill, 2008-04-17)
• 5. The Prime Number Theorem (pnt, by Mario Carneiro, 2016-06-01) - also see pnt2, pnt3
• 7. Law of Quadratic Reciprocity (lgsquad, by Mario Carneiro, 2015-06-19)
• 9. The Area of a Circle (areacirc, by Brendan Leahy, 2017-08-31)
• 10. Euler's Generalization of Fermat's Little Theorem (eulerth, by Mario Carneiro, 2014-02-28). The intuitionistic logic explorer (iset.mm) database also includes eulerth (by Jim Kingdon, 2024-09-07)
• 11. The Infinitude of Primes (infpn2, by Norman Megill, 2005-05-05). The intuitionistic logic explorer (iset.mm) database also includes infpn2 (by Jim Kingdon, 2024-10-26)
• 14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + .... (basel, by Mario Carneiro, 2014-07-30)
• 15. The Fundamental Theorem of Integral Calculus (ftc1 and ftc2, by Mario Carneiro, 2014-09-03)
• 17. De Moivre's Theorem (demoivreALT, by Steve Rodriguez, 2006-11-10). See also the later proof demoivre (by Norman Megill, 2007-07-24), which is shorter and more general but uses the exponential function. The intuitionistic logic explorer (iset.mm) database includes both proofs as demoivreALT and demoivre (added 2023-01-04).
• 18. Liouville's Theorem and the Construction of Transcendental Numbers (aaliou, by Stefan O'Rear, 2014-11-22)
• 19. Four Squares Theorem (4sq, by Mario Carneiro, 2014-07-16)
• 20. All Primes (1 mod 4) Equal the Sum of Two Squares (2sq, by Mario Carneiro, 2015-06-20)
• 22. The Non-Denumerability of the Continuum (ruc, by Norman Megill, 2004-08-13)
• 23. Formula for Pythagorean Triples (pythagtrip, by Scott Fenton, 2014-04-19). The intuitionistic logic explorer (iset.mm) database also includes pythagtrip (added by Jim Kingdon, 2024-10-04).
• 25. Schroeder-Bernstein Theorem (sbth, by Norman Megill, 1998-06-08). The intuitionistic logic explorer (iset.mm) database shows that Schroeder-Bernstein is equivalent to excluded middle, resolving this problem in the negative, at exmidsbth (by Jim Kingdon, 2022-08-13).
• 26. Leibniz' Series for Pi (leibpi, by Mario Carneiro, 2015-04-16)
• 27. Sum of the Angles of a Triangle (ang180, by Mario Carneiro, 2014-09-24)
• 30. The Ballot Problem (aka Bertrand's ballot problem) (ballotth, by Thierry Arnoux, contributed 2016-12-07)
• 31. Ramsey's Theorem (ramsey, by Mario Carneiro, 2015-04-23)
• 34. Divergence of the Harmonic Series (harmonic, by Mario Carneiro, 2014-07-11)
• 35. Taylor's Theorem (taylth, by Mario Carneiro, 2017-01-01)
• 37. The Solution of a Cubic (cubic, by Mario Carneiro, 2015-04-26)
• 38. Arithmetic Mean/Geometric Mean (amgm, by Mario Carneiro, 2015-06-21)
• 39. Solutions to Pell's Equation (rmxycomplete, by Stefan O'Rear, 2014-11-22)
• 42. Sum of the Reciprocals of the Triangular Numbers (trirecip, by Scott Fenton, 2014-05-02). The intuitionistic logic explorer (iset.mm) database includes this proof as trirecip (added 2022-10-22).
• 44. The Binomial Theorem (binom, Norman Megill, 2005-12-07). The intuitionistic logic explorer (iset.mm) database includes this proof as binom (added 2022-10-15).
• 45. The Partition Theorem (by Euler) (eulerpart, Thierry Arnoux, 2018-08-30)
• 46. The Solution of the General Quartic Equation (quart, by Mario Carneiro, 2015-05-06)
• 48. Dirichlet's Theorem (dirith, by Mario Carneiro, 2016-05-12)
• 49. The Cayley-Hamilton Theorem (cayleyhamilton, by Alexander van der Vekens, 2019-11-25)
• 51. Wilson's Theorem (wilth, by Mario Carneiro, 2015-01-28)
• 52. The Number of Subsets of a Set (pw2en, by Norman Megill, 2004-01-29)
• 54. The Konigsberg Bridge Problem (konigsberg, by Mario Carneiro, 2015-04-16)
• 55. Product of Segments of Chords (chordthm by David Moews, 2017-02-28)
• 57. Heron's Formula (heron by Mario Carneiro based on work by Jon Pennant and Thierry Arnoux, 2019-03-10)
• 58. Formula for the Number of Combinations (hashbc, by Mario Carneiro, 2014-07-13)
• 60. Bezout's Theorem (bezout, by Mario Carneiro, 2014-02-22). The intuitionistic logic explorer (iset.mm) database also includes bezout (by Mario Carneiro and Jim Kingdon, 2022-01-09).
• 61. Theorem of Ceva (cevath, by Saveliy Skresanov, 2017-09-24)
• 63. Cantor's Theorem (canth2, by Norman Megill, 1994-08-07)
• 64. L'Hôpital's Rule (lhop, by Mario Carneiro, 2016-12-30)
• 65. Isosceles Triangle Theorem (isosctr, by Saveliy Skresanov, 2017-01-01)
• 66. Sum of a Geometric Series (geoser, by Norman Megill, 2006-05-09). The intuitionistic logic explorer (iset.mm) database includes this proof as geoserap (added 2022-10-24).
• 67. e is Transcendental (etransc, by Glauco Siliprandi, 2020-04-05)
• 68. Sum of an arithmetic series (arisum, by Frédéric Liné, 2006-11-16) - arisum is not fully general, but it would be straightforward to enhance. The intuitionistic logic explorer (iset.mm) database includes this proof as arisum (added 2022-10-22).
• 69. Greatest Common Divisor Algorithm (eucalg, by Paul Chapman, 2011-03-31). The intuitionistic logic explorer (iset.mm) database includes this proof as eucalg (by Jim Kingdon, 2022-01-11).
• 70. The Perfect Number Theorem (perfect, by Mario Carneiro, 2016-05-17)
• 71. Order of a Subgroup (lagsubg, by Mario Carneiro, 2014-07-11) - also see lagsubg2
• 72. Sylow's Theorem (sylow1 and sylow2 and sylow2b and sylow3, by Mario Carneiro, 2015-01-19)
• 73. Ascending or Descending Sequences (erdsze and erdsze2, by Mario Carneiro, 2015-01-28)
• 74. The Principle of Mathematical Induction (finds, by Norman Megill, 1995-04-14). There are many versions of Mathematical Induction in set.mm. Theorem findes (by Raph Levien, 2003-07-09) is a compact and more traditional-looking version with explicit substitution. Another alternative is nnind (by Norman Megill, 1997-01-10), which uses natural numbers instead of ordinal numbers and might be less obscure for non-mathematicians. The intuitionistic logic explorer (iset.mm) database also includes finds (adapted from Norman Megill's set.mm proof by Jim Kingdon, 2018-12-01) proved from IZF (intuitionistic Zermelo--Fraenkel) and bj-findes (by Benoit Jubin, 2019-11-21) proved from CZF (constructive Zermelo--Fraenkel).
• 75. The Mean Value Theorem (mvth, by Mario Carneiro, 2014-09-14)
• 76. Fourier Series (fourier, by Glauco Siliprandi, 2019-12-11)
• 77. Sum of kth powers (fsumkthpow, by Scott Fenton, 2014-05-16)
• 78. The Cauchy-Schwarz Inequality (ipcau, by Norman Megill, 2008-01-12)
• 79. The Intermediate Value Theorem (ivth, by Paul Chapman, 2008-01-22). The intuitionistic logic explorer (iset.mm) database also includes ivthinc which is the theorem for a strictly monotonic function (by Jim Kingdon, 2024-02-20).
• 80. Fundamental Theorem of Arithmetic (1arith2, by Paul Chapman, 2012-11-17). The intuitionistic logic explorer (iset.mm) database also includes 1arith2 (added by Jim Kingdon, 2024-10-31).
• 81. Erdős's proof of the divergence of the inverse prime series (prmrec, by Mario Carneiro, 2014-08-10)
• 83. The Friendship Theorem (friendship, by Alexander van der Vekens, 2018-10-09)
• 85. Divisibility by 3 Rule (3dvds, by Mario Carneiro, 2014-07-14)
• 86. Lebesgue Measure and Integration (itgcl, by Mario Carneiro, 2014-06-29)
• 87. Desargues's Theorem (dath, by Norman Megill, 2012-08-20)
• 88. Derangements Formula (derangfmla and subfaclim, by Mario Carneiro, 2015-01-28)
• 89. The Factor and Remainder Theorems (facth and plyrem, by Mario Carneiro, 2014-07-26)
• 90. Stirling's Formula (stirling by Glauco Siliprandi, 2017-06-29)
• 91. The Triangle Inequality (abstrii, by Norman Megill, 1999-10-02). The intuitionistic logic explorer (iset.mm) database includes this proof as abstrii (added 2021-08-13).
• 93. The Birthday Problem (birthday, by Mario Carneiro, 2015-04-17)
• 94. The Law of Cosines (lawcos, by David A. Wheeler, 2015-06-12)
• 95. Ptolemy's Theorem (ptolemy, by David A. Wheeler, 2015-05-31). The intuitionistic logic explorer (iset.mm) database includes this proof as ptolemy (added 2024-03-12).
• 96. Principle of Inclusion/Exclusion (incexc, by Mario Carneiro, 2017-08-07)
• 97. Cramer's Rule (cramer, by Alexander van der Vekens, 2019-02-21, which built on the key work on determinants by Stefan O'Rear)
• 98. Bertrand's Postulate (bpos, by Mario Carneiro, 2014-03-15)

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

• Every vector space is free (lbsex, by Mario Carneiro, 2014-06-25)
• Heine-Borel Theorem (heibor, by Jeff Madsen, 2009-09-02) - also see cnheibor
• Hilbert Basis Theorem (hbt, by Stefan O'Rear, 2015-04-04)
• Stone-Weierstrass Theorem (stowei, by Glauco Siliprandi, 2017-04-20)

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

• 6. Gödel's Incompleteness Theorem
• 8. The Impossibility of Trisecting the Angle and Doubling the Cube
• 12. The Independence of the Parallel Postulate
• 13. Polyhedron Formula
• 16. Insolvability of General Higher Degree Equations
• 21. Green's Theorem
• 24. The Undecidability of the Continuum Hypothesis
• 28. Pascal's Hexagon Theorem
• 29. Feuerbach's Theorem
• 32. The Four Color Problem
• 33. Fermat's Last Theorem
• 36. Brouwer Fixed Point Theorem
• 40. Minkowski's Fundamental Theorem
• 41. Puiseux's Theorem
• 43. The Isoperimetric Theorem
• 47. The Central Limit Theorem
• 50. The Number of Platonic Solids
• 53. π is Transcendental
• 56. The Hermite-Lindemann Transcendence Theorem
• 59. The Laws of Large Numbers
• 62. Fair Games Theorem
• 82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
• 84. Morley's Theorem
• 92. Pick's Theorem
• 99. Buffon Needle Problem
• 100. Descartes Rule of Signs

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.