Formalizing 100 Theorems

There used to exist a "top 100" of mathematical theorems on the web, which is a rather arbitrary list (and most of the theorems seem rather elementary), but still is nice to look at. On the current page I will keep track of which theorems from this list have been formalized. Currently the fraction that already has been formalized seems to be

99%

The page does not keep track of all formalizations of these theorems. It just shows formalizations in systems that have formalized a significant number of theorems, or that have formalized a theorem that none of the others have done. The systems that this page refers to are (in order of the number of theorems that have been formalized, so the more interesting systems for mathematics are near the top):

Isabelle 90
HOL Light 87
Coq 79
Lean 76
Metamath 74
Mizar 69
nqthm/ACL2 47
ProofPower 43
PVS 26
Megalodon 12
Naproche 10
NuPRL/MetaPRL 8

Theorems in the list which have not been formalized yet are in italics. Formalizations of constructive proofs are in italics too. The difficult proofs in the list (according to John all the others are not a serious challenge "given a week or two") have been underlined. The formalizations under a theorem are in the order of the list of systems, and not in chronological order.

The List

  1. The Irrationality of the Square Root of 2
    • Isabelle, Markus Wenzel: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, many versions: statement
    • Lean, mathlib: statement
    • Metamath, Norman Megill: statement
    • Mizar, Freek Wiedijk: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
    • PVS, Bart Jacobs & John Rushby
    • Megalodon: statement
    • Naproche, Peter Koepke, Mateusz Marcol & Patrick Schäfer
    • NuPRL, Stuart Allen, Paul Jackson
  2. Fundamental Theorem of Algebra
  3. The Denumerability of the Rational Numbers
    • Isabelle, Stefan Richter & Benjamin Porter: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Yves Bertot & Milad Niqui: statement
    • Lean, Chris Hughes: statement
    • Metamath, revised by Mario Carneiro: statement
    • Mizar, Grzegorz Bancerek: statement
    • ACL2, David M. Russinoff
    • ProofPower, Rob Arthan: statement
    • PVS, Jerry James
    • Megalodon: statement
    • NuPRL, Stuart Allen
  4. Pythagorean Theorem
  5. Prime Number Theorem
  6. Gödel's Incompleteness Theorem
    • Isabelle, Larry Paulson: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Russell O'Connor: statement
    • nqthm, Natarajan Shankar
  7. Law of Quadratic Reciprocity
  8. The Impossibility of Trisecting the Angle and Doubling the Cube
  9. The Area of a Circle
    • Isabelle, Manuel Eberl: statement
    • HOL Light, John Harrison: statements
    • Lean, James Arthur & Benjamin Davidson & Andrew Souther: statement
    • Metamath, Brendan Leahy: statement
    • ACL2, Jagadish Bapanapally
    • ProofPower, Rob Arthan: statement
  10. Euler's Generalization of Fermat's Little Theorem
    • Isabelle, Thomas M. Rasmussen, Amine Chaieb: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Laurent Théry: statement
    • Lean, Chris Hughes: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Yoshinori Fujisawa & Yasushi Fuwa & Hidetaka Shimizu: statement
    • ACL2, David M. Russinoff
  11. The Infinitude of Primes
    • Isabelle, Jacques D. Fleuriot: statement
    • HOL Light, John Harrison: statement
    • Coq, not in contribs, Russell O'Connor: statement
    • Lean, Jeremy Avigad: statement
    • Metamath, Norman Megill: statement
    • Mizar, Rafal Kwiatek: statement
    • ACL2, David M. Russinoff
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
    • Megalodon: statement
    • Naproche, Peter Koepke
  12. The Independence of the Parallel Postulate
  13. Polyhedron Formula
  14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
  15. Fundamental Theorem of Integral Calculus
    • Isabelle, Jacques D. Fleuriot: statement
    • HOL Light, John Harrison: statement
    • Coq, C-CoRN, Luís Cruz-Filipe: statement
    • Lean, Yury G. Kudryashov (first) and Benjamin Davidson (second): statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Noboru Endou & Katsumi Wasaki & Yasunari Shidama: statement
    • ACL2, Matt Kaufmann
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
  16. Insolvability of General Higher Degree Equations
    • Coq, Sophie Bernard & Cyril Cohen & Assia Mahboubi & Pierre-Yves Strub, statement
    • Lean, Thomas Browning: statement
  17. De Moivre's Theorem
    • Isabelle, Jacques D. Fleuriot: statements
    • HOL Light, John Harrison: statement
    • Coq, contrib, Frédérique Guilhot: statement
    • Lean, Abhimanyu Pallavi Sudhir: statement
    • Metamath, Steve Rodriguez: statement
    • Mizar, Takashi Mitsuishi & Noboru Endou & Keiji Ohkubo: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
  18. Liouville's Theorem and the Construction of Transcendental Numbers
  19. Four Squares Theorem
    • Isabelle, Roelof Oosterhuis: statement
    • HOL Light, John Harrison: statement
    • Coq, Guillaume Allais & Jean-Marie Madiot: statement
    • Lean, Chris Hughes: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Yasushige Watase: statement
    • ACL2, David M. Russinoff
    • PVS, Anthony Narkawicz
  20. All Primes (1 mod 4) Equal the Sum of Two Squares
  21. Green's Theorem
    • Isabelle, Mohammad Abdulaziz & Larry Paulson: statement
  22. The Non-Denumerability of the Continuum
  23. Formula for Pythagorean Triples
  24. The Undecidability of the Continuum Hypothesis
    • Isabelle, Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf & Matías Steinberg: statement
    • Lean, Jesse Han & Floris van Doorn: statement
  25. Schroeder-Bernstein Theorem
    • Isabelle, Tobias Nipkow: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Hugo Herbelin: statement
    • Lean, Mario Carneiro: statement
    • Metamath, Norman Megill and Jim Kingdon: statement
    • Mizar, Piotr Rudnicki & Andrzej Trybulec: statement
    • ACL2, Grant Jurgensen
    • ProofPower, Rob Arthan: statement
    • Megalodon: statement
    • Naproche, Peter Koepke & Marcel Schütz
  26. Leibniz's Series for Pi
  27. Sum of the Angles of a Triangle
  28. Pascal's Hexagon Theorem
  29. Feuerbach's Theorem
  30. The Ballot Problem
  31. Ramsey's Theorem
  32. The Four Color Problem
    • Coq, not in contribs, Georges Gonthier: statement
  33. Fermat's Last Theorem
  34. Divergence of the Harmonic Series
    • Isabelle, Benjamin Porter: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Frédérique Guilhot: statement
    • Lean, Anatole Dedecker: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement
    • ACL2, David M. Russinoff
    • ProofPower, Rob Arthan: statement
    • PVS, Greg Anderson
  35. Taylor's Theorem
    • Isabelle, Jacques D. Fleuriot & Lukas Bulwahn & Bernhard Häupler: statement
    • HOL Light, John Harrison: statement
    • Coq, C-CoRN, Luís Cruz-Filipe: statement
    • Lean, Moritz Doll: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Yasunari Shidama: statement
    • ACL2, Ruben Gamboa & Brittany Middleton & Jun Sawada
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
  36. Brouwer Fixed Point Theorem
  37. The Solution of a Cubic
  38. Arithmetic Mean/Geometric Mean
  39. Solutions to Pell's Equation
  40. Minkowski's Fundamental Theorem
  41. Puiseux's Theorem
    • Isabelle, Manuel Eberl: statement
    • Coq, not yet in contrib, Daniel de Rauglaudre: statement
  42. Sum of the Reciprocals of the Triangular Numbers
  43. The Isoperimetric Theorem
  44. The Binomial Theorem
  45. The Partition Theorem
  46. The Solution of the General Quartic Equation
  47. The Central Limit Theorem
  48. Dirichlet's Theorem
  49. The Cayley-Hamilton Theorem
    • Isabelle, Stephan Adelsberger, Stefan Hetzl & Florian Pollak: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Sidi Ould Biha: statement
    • Lean, Scott Morrison: statement
    • Metamath, Alexander van der Vekens: statement
  50. The Number of Platonic Solids
  51. Wilson's Theorem
  52. The Number of Subsets of a Set
  53. Pi is Transcendental
  54. Konigsberg Bridges Problem
  55. Product of Segments of Chords
  56. The Hermite-Lindemann Transcendence Theorem
  57. Heron's Formula
  58. Formula for the Number of Combinations
  59. The Laws of Large Numbers
  60. Bezout's Theorem
  61. Theorem of Ceva
  62. Fair Games Theorem
  63. Cantor's Theorem
  64. L'Hôpital's Rule
  65. Isosceles Triangle Theorem
  66. Sum of a Geometric Series
    • Isabelle, Jacques D. Fleuriot: statements
    • HOL Light, John Harrison: statements
    • Coq, C-CoRN, Luís Cruz-Filipe: statement
    • Lean, Sander R. Dahmen (finite) and Johannes Hölzl (infinite): statement
    • Metamath, Norman Megill: statement
    • Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
    • Naproche, Peter Koepke
  67. e is Transcendental
  68. Sum of an arithmetic series
    • Isabelle, Benjamin Porter: statement
    • HOL Light, John Harrison: statement
    • Coq, not in contribs, many versions: statement
    • Lean, Johannes Hölzl: statement
    • Metamath, Frédéric Liné: statement
    • Mizar, Ming Liang & Yuzhong Ding: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Tanner Slagel
    • Naproche, Peter Koepke
  69. Greatest Common Divisor Algorithm
    • Isabelle, Larry Paulson: statement
    • HOL Light, John Harrison: statements
    • Coq, standard library: statement
    • Lean, mathlib: statement
    • Metamath, Paul Chapman: statement
    • Mizar, Grzegorz Bancerek: statement
    • ACL2, David M. Russinoff
    • ProofPower, Rob Arthan: statement
    • PVS, Kai Engelhardt
    • NuPRL, Paul Jackson & Rich Eaton
    • Megalodon: statement
    • Naproche, Mateusz Marcol & Patrick Schäfer
  70. The Perfect Number Theorem
  71. Order of a Subgroup
    • Isabelle, Florian Kammüller: statement
    • HOL Light, John Harrison: statement
    • Coq, almost C-CoRN, Dan Synek & contrib, Laurent Théry: statement
    • Lean, mathlib: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Wojciech Trybulec: statement
    • ACL2, David M. Russinoff
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, David Lester
  72. Sylow's Theorem
  73. Ascending or Descending Sequences
  74. The Principle of Mathematical Induction
  75. The Mean Value Theorem
    • Isabelle, Jacques D. Fleuriot: statement
    • HOL Light, John Harrison: statement
    • Coq, C-CoRN, Luís Cruz-Filipe: statement
    • Lean, Yury G. Kudryashov: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Jaroslaw Kotowicz & Konrad Raczkowski & Pawel Sadowski: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Bruno Dutertre
  76. Fourier Series
  77. Sum of kth powers
  78. The Cauchy-Schwarz Inequality
  79. The Intermediate Value Theorem
    • Isabelle, Jacques D. Fleuriot: statement
    • HOL Light, John Harrison: statement
    • Coq, C-CoRN, Herman Geuvers et al.: statement
    • Lean, mathlib: statement
    • Metamath, Paul Chapman: statement
    • Mizar, Yatsuka Nakamura & Andrzej Trybulec: statement
    • ACL2, Ruben Gamboa
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Bruno Dutertre
  80. The Fundamental Theorem of Arithmetic
    • Isabelle, Thomas M. Rasmussen: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Martijn Oostdijk: statement
    • Lean, mathlib: statement
    • Metamath, Paul Chapman: statement
    • Mizar, Artur Korniłowicz, Piotr Rudnicki & Hiroyuki Okazaki, Yasunari Shidama: statements
    • ACL2, John Cowles
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
    • Megalodon: statement
    • NuPRL, Stuart Allen & Paul Jackson
  81. Divergence of the Prime Reciprocal Series
  82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
  83. The Friendship Theorem
  84. Morley's Theorem
  85. Divisibility by 3 Rule
  86. Lebesgue Measure and Integration
    • Isabelle, Stefan Richter: statement
    • HOL Light, John Harrison: statement
    • Coq, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin & Micaela Mayero, and Reynald Affeldt & Cyril Cohen: statement
    • Lean, Johannes Hölzl: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Noboru Endou & Yasunari Shidama: statement
  87. Desargues's Theorem
    • Isabelle, Anthony Bordg: statement
    • HOL Light, John Harrison: statement
    • Coq, contrib, Frédérique Guilhot, Julien Narboux: statement
    • Metamath, Norman Megill: statement
    • Mizar, Wojciech Leonczuk & Krzysztof Prazmowski: statement
  88. Derangements Formula
  89. The Factor and Remainder Theorems
  90. Stirling's Formula
    • Isabelle, Manuel Eberl: statements
    • HOL Light, John Harrison: statement
    • Coq, not in contribs, Coqtail team: statement
    • Lean, mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth): statement
    • Metamath, Glauco Siliprandi: statement
  91. The Triangle Inequality
  92. Pick's Theorem
    • Isabelle, Sage Binder & Katherine Kosaian: statement
    • HOL Light, John Harrison: statement
  93. The Birthday Problem
  94. The Law of Cosines
  95. Ptolemy's Theorem
  96. Principle of Inclusion/Exclusion
  97. Cramer's Rule
    • Isabelle, Amine Chaieb: statement
    • HOL Light, John Harrison: statement
    • Coq, not in contribs, Georges Gonthier et al.: statement
    • Lean, Anne Baanen: statement
    • Metamath, Alexander van der Vekens (based on work by Stefan O'Rear): statement
    • Mizar, Karol Pak: statement
    • ACL2, David M. Russinoff
  98. Bertrand's Postulate
  99. Buffon Needle Problem
  100. Descartes Rule of Signs

This list (which I did not make!) has some obvious omissions. I will list here, in alphabetical order, the theorems that people have complained to me are missing. (Some of them might just be missing because they are "too new", as the list is from 1999.)

(last modification 2024-09-10)