Formalizing 100 Theorems

There is 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 keep track of which theorems from this list have been formalized. Currently the fraction that already has been formalized seems to be

100%

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

Lean 100
HOL Light 99
Isabelle 95
Rocq 80
Metamath 75
Mizar 71
nqthm/ACL2 48
ProofPower 43
PVS 26
Imandra 20
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
  2. Fundamental Theorem of Algebra
  3. The Denumerability of the Rational Numbers
  4. Pythagorean Theorem
  5. Prime Number Theorem
    • Lean, Alex Kontorovich, Terry Tao, and the Prime Number Theorem + Project: statement
    • HOL Light, John Harrison: statement
    • Isabelle, Jeremy Avigad et al.: statement
    • Metamath, Mario Carneiro: statement
  6. Gödel's Incompleteness Theorem
  7. Law of Quadratic Reciprocity
  8. The Impossibility of Trisecting the Angle and Doubling the Cube
  9. The Area of a Circle
  10. Euler's Generalization of Fermat's Little Theorem
  11. The Infinitude of Primes
  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
    • Lean, Yury G. Kudryashov (first) and Benjamin Davidson (second): statement
    • HOL Light, John Harrison: statement
    • Isabelle, Jacques D. Fleuriot: statement
    • Rocq, C-CoRN, Luís Cruz-Filipe: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Noboru Endou & Katsumi Wasaki & Yasunari Shidama: statement
    • ACL2, Matt Kaufmann: statement
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
  16. Insolvability of General Higher Degree Equations
    • Lean, Thomas Browning: statement
    • HOL Light, John Harrison: statement
    • Rocq, Sophie Bernard & Cyril Cohen & Assia Mahboubi & Pierre-Yves Strub: statement
  17. De Moivre's Theorem
  18. Liouville's Theorem and the Construction of Transcendental Numbers
  19. Four Squares Theorem
  20. All Primes (1 mod 4) Equal the Sum of Two Squares
  21. Green's Theorem
    • Lean, the Tau Ceti contributors: statement
    • HOL Light, Claude Code with John Harrison: statement
    • 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
    • Lean, Jesse Han & Floris van Doorn: statement
    • HOL Light, Claude Code: statement
    • Isabelle, Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf & Matías Steinberg: statement
  25. Schroeder-Bernstein Theorem
  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
  33. Fermat's Last Theorem
  34. Lean, Anthropic: statement
  35. Divergence of the Harmonic Series
  36. Taylor's Theorem
    • Lean, Moritz Doll: statement
    • HOL Light, John Harrison: statement
    • Isabelle, Jacques D. Fleuriot & Lukas Bulwahn & Bernhard Häupler: statement
    • Rocq, C-CoRN, Luís Cruz-Filipe: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Yasunari Shidama: statement
    • ACL2, Ruben Gamboa & Brittany Middleton & Jun Sawada: statement
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
  37. Brouwer Fixed Point Theorem
  38. The Solution of a Cubic
  39. Arithmetic Mean/Geometric Mean
  40. Solutions to Pell's Equation
  41. Minkowski's Fundamental Theorem
  42. Puiseux's Theorem
  43. Sum of the Reciprocals of the Triangular Numbers
  44. The Isoperimetric Theorem
  45. The Binomial Theorem
  46. The Partition Theorem
  47. The Solution of the General Quartic Equation
  48. The Central Limit Theorem
  49. Dirichlet's Theorem
  50. The Cayley-Hamilton Theorem
    • Lean, Scott Morrison: statement
    • HOL Light, John Harrison: statement
    • Isabelle, Stephan Adelsberger, Stefan Hetzl & Florian Pollak: statement
    • Rocq, contrib, Sidi Ould Biha: statement
    • Metamath, Alexander van der Vekens: statement
  51. The Number of Platonic Solids
  52. Wilson's Theorem
  53. The Number of Subsets of a Set
  54. Pi is Transcendental
  55. Konigsberg Bridges Problem
  56. Product of Segments of Chords
  57. The Hermite-Lindemann Transcendence Theorem
  58. Heron's Formula
  59. Formula for the Number of Combinations
  60. The Laws of Large Numbers
  61. Bezout's Theorem
  62. Theorem of Ceva
  63. Fair Games Theorem
  64. Cantor's Theorem
  65. L'Hôpital's Rule
  66. Isosceles Triangle Theorem
  67. Sum of a Geometric Series
    • Lean, Sander R. Dahmen (finite) and Johannes Hölzl (infinite): statement
    • HOL Light, John Harrison: statements
    • Isabelle, Jacques D. Fleuriot: statements
    • Rocq, C-CoRN, Luís Cruz-Filipe: statement
    • Metamath, Norman Megill: statement
    • Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement
    • ACL2, Ruben Gamboa: statement
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Ricky Butler
    • Imandra: statement
    • Naproche, Peter Koepke
  68. e is Transcendental
  69. Sum of an arithmetic series
  70. Greatest Common Divisor Algorithm
  71. The Perfect Number Theorem
  72. Order of a Subgroup
  73. Sylow's Theorem
  74. Ascending or Descending Sequences
  75. The Principle of Mathematical Induction
  76. The Mean Value Theorem
    • Lean, Yury G. Kudryashov: statement
    • HOL Light, John Harrison: statement
    • Isabelle, Jacques D. Fleuriot: statement
    • Rocq, C-CoRN, Luís Cruz-Filipe: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Jaroslaw Kotowicz & Konrad Raczkowski & Pawel Sadowski: statement
    • ACL2, Ruben Gamboa: statement
    • ProofPower, Rob Arthan: statement
    • PVS, NASA library, Bruno Dutertre
  77. Fourier Series
  78. Sum of kth powers
  79. The Cauchy-Schwarz Inequality
  80. The Intermediate Value Theorem
  81. The Fundamental Theorem of Arithmetic
  82. Divergence of the Prime Reciprocal Series
  83. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
  84. The Friendship Theorem
  85. Morley's Theorem
  86. Divisibility by 3 Rule
  87. Lebesgue Measure and Integration
    • Lean, Johannes Hölzl: statement
    • HOL Light, John Harrison: statement
    • Isabelle, Stefan Richter: statement
    • Rocq, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin & Micaela Mayero, and Reynald Affeldt & Cyril Cohen: statement
    • Metamath, Mario Carneiro: statement
    • Mizar, Noboru Endou & Yasunari Shidama: statement
  88. Desargues's Theorem
  89. Derangements Formula
  90. The Factor and Remainder Theorems
  91. Stirling's Formula
    • Lean, mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth): statement
    • HOL Light, John Harrison: statement
    • Isabelle, Manuel Eberl: statements
    • Rocq, not in contribs, Coqtail team: statement
    • Metamath, Glauco Siliprandi: statement
  92. The Triangle Inequality
  93. Pick's Theorem
  94. The Birthday Problem
  95. The Law of Cosines
  96. Ptolemy's Theorem
  97. Principle of Inclusion/Exclusion
  98. Cramer's Rule
  99. Bertrand's Postulate
  100. Buffon Needle Problem
  101. 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 2026-11-01)