# 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

93%

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

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
• HOL Light, John Harrison: statement
• Isabelle, Markus Wenzel: statement
• Coq, contrib, many versions: statement
• Mizar, Freek Wiedijk: statement
• Metamath, Norman Megill: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• PVS, Bart Jacobs & John Rushby
• NuPRL, Stuart Allen, Paul Jackson
2. Fundamental Theorem of Algebra
3. The Denumerability of the Rational Numbers
• HOL Light, John Harrison: statement
• Isabelle, Stefan Richter & Benjamin Porter: statement
• Coq, contrib, Yves Bertot & Milad Niqui: statement
• Mizar, Grzegorz Bancerek: statement
• Metamath, revised by Mario Carneiro: statement
• ProofPower, Rob Arthan: statement
• NuPRL, Stuart Allen
4. Pythagorean Theorem
5. Prime Number Theorem
6. Gödel's Incompleteness Theorem
• HOL Light, John Harrison: statement
• Isabelle, Larry Paulson: statement
• Coq, contrib, Russell O'Connor: statement
• nqthm, Natarajan Shankar
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
• HOL Light, John Harrison: statement
• Isabelle, Thomas M. Rasmussen, Amine Chaieb: statement
• Coq, contrib, Laurent Théry: statement
• Mizar, Yoshinori Fujisawa & Yasushi Fuwa & Hidetaka Shimizu: statement
• Metamath, Mario Carneiro: statement
11. The Infinitude of Primes
• HOL Light, John Harrison: statement
• Isabelle, Jacques D. Fleuriot: statement
• Coq, not in contribs, Russell O'Connor: statement
• Mizar, Rafal Kwiatek: statement
• ProofPower, Rob Arthan: statement
• ACL2, David Russinoff
• Metamath, Norman Megill: statement
• PVS, NASA library, Ricky Butler
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
• HOL Light, John Harrison: statement
• Isabelle, Jacques D. Fleuriot: statement
• Coq, C-CoRN, Luís Cruz-Filipe: statement
• Mizar, Noboru Endou & Katsumi Wasaki & Yasunari Shidama: statement
• Metamath, Mario Carneiro: statement
• ProofPower, Rob Arthan: statement
• ACL2, Matt Kaufmann
• PVS, NASA library, Ricky Butler
16. Insolvability of General Higher Degree Equations
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
• Isabelle, Mohammad Abdulaziz & Lawrence Paulson: statement
22. The Non-Denumerability of the Continuum
23. Formula for Pythagorean Triples
24. The Undecidability of the Continuum Hypothesis
25. Schroeder-Bernstein Theorem
26. Leibniz's Series for Pi
• HOL Light, John Harrison: statement
• Isabelle, Johannes Hoelzl: statement
• Coq, standard library & C-CoRN, Luís Cruz-Filipe: statement
• Mizar, Karol Pak: statement
• Metamath, Mario Carneiro: statement
• PVS, NASA library, David Lester
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
• HOL Light, John Harrison: statement
• Isabelle, Tom Ridge: statement
• Mizar, Marco Riccardi: statement
• Metamath, Mario Carneiro: statement
• ProofPower, Rob Arthan & Roger Bishop Jones: statement
• PVS, NASA library, Natarajan Shankar
• nqthm, Matt Kaufmann
• NuPRL, David Basin
32. The Four Color Problem
• Coq, not in contribs, Georges Gonthier: statement
33. Fermat's Last Theorem
34. Divergence of the Harmonic Series
35. Taylor's Theorem
• HOL Light, John Harrison: statement
• Isabelle, Jacques D. Fleuriot & Lukas Bulwahn & Bernhard Häupler: statement
• Coq, C-CoRN, Luís Cruz-Filipe: statement
• Mizar, Yasunari Shidama: statement
• Metamath, Mario Carneiro: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa & Brittany Middleton & Jun Sawada
• 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
• 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
• HOL Light, John Harrison: statement
• Isabelle, Tobias Nipkow: statement
• Coq, contrib, Laurent Théry: statement
• Mizar, Christoph Schwarzweller: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• Metamath, Norman Megill: statement
• NuPRL, Paul Jackson & Rich Eaton
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
• HOL Light, John Harrison: statement
• Isabelle, Stephan Adelsberger, Stefan Hetzl & Florian Pollak: statement
• Coq, contrib, Sidi Ould Biha: statement
50. The Number of Platonic Solids
51. Wilson's Theorem
52. The Number of Subsets of a Set
53. Pi is Transcendental
• Coq, Sophie Bernard & Laurence Rideau: statement
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
• HOL Light, John Harrison: statements
• Isabelle, Jacques D. Fleuriot: statements
• Coq, C-CoRN, Luís Cruz-Filipe: statement
• Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• Metamath, Norman Megill: statement
• PVS, NASA library, Ricky Butler
67. e is Transcendental
68. Sum of an arithmetic series
69. Greatest Common Divisor Algorithm
70. The Perfect Number Theorem
71. Order of a Subgroup
• HOL Light, John Harrison: statement
• Isabelle, Florian Kammüller: statement
• Coq, almost C-CoRN, Dan Synek & contrib, Laurent Théry: statement
• Mizar, Wojciech Trybulec: statement
• Metamath, Mario Carneiro: statement
• 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
• HOL Light, John Harrison: statement
• Isabelle, Jacques D. Fleuriot: statement
• Coq, C-CoRN, Luís Cruz-Filipe: statement
• Metamath, Mario Carneiro: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• PVS, NASA library, Bruno Dutertre
76. Fourier Series
77. Sum of kth powers
78. The Cauchy-Schwarz Inequality
79. The Intermediate Value Theorem
• HOL Light, John Harrison: statement
• Isabelle, Jacques D. Fleuriot: statement
• Coq, C-CoRN, Herman Geuvers et al.: statement
• Mizar, Yatsuka Nakamura & Andrzej Trybulec: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• Metamath, Paul Chapman: statement
• PVS, NASA library, Bruno Dutertre
80. The Fundamental Theorem of Arithmetic
• HOL Light, John Harrison: statement
• Isabelle, Thomas M. Rasmussen: statement
• Coq, contrib, Martijn Oostdijk: statement
• Mizar, Artur Korniłowicz, Piotr Rudnicki & Hiroyuki Okazaki, Yasunari Shidama: statements
• Metamath, Paul Chapman: statement
• ProofPower, Rob Arthan: statement
• ACL2, John Cowles
• PVS, NASA library, Ricky Butler
• 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
87. Desargues's Theorem
• HOL Light, John Harrison: statement
• Coq, contrib, Frédérique Guilhot, Julien Narboux: statement
• Mizar, Wojciech Leonczuk & Krzysztof Prazmowski: statement
• Metamath, Norman Megill: statement
88. Derangements Formula
89. The Factor and Remainder Theorems
90. Stirling's Formula
91. The Triangle Inequality
• HOL Light, John Harrison: statement
• Isabelle, Steven Obua: statement
• Coq, Frédérique Guilhot: statement
• Mizar, Czeslaw Bylinski: statement
• ProofPower, Rob Arthan: statement
• ACL2, Ruben Gamboa
• Metamath, Norman Megill: statement
• PVS, NASA library, Ricky Butler & Cesar Munoz
92. Pick's Theorem
93. The Birthday Problem
94. The Law of Cosines
• HOL Light, John Harrison: statement
• Isabelle, Manuel Eberl: statement
• Coq, contrib, Frédérique Guilhot: statement
• Mizar, Marco Riccardi: statement
• Metamath, David A. Wheeler: statement
• PVS, NASA library, Cesar Munoz & Ricky Butler
95. Ptolemy's Theorem
96. Principle of Inclusion/Exclusion
97. Cramer's Rule
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.)
• Atiyah-Singer Index Theorem
• Baker's Theorem on Linear Forms in Logarithms
• Black-Scholes Formula
• Borsuk-Ulam Theorem
• Cauchy's Integral Theorem
• Cauchy's Residue Theorem
• Chen's theorem
• every vector space is free
• Classification of Finite Simple Groups
• Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
• Sophie Germain's theorem
• Gödel's Completeness Theorem
• Gödel's Second Incompleteness Theorem
• Green-Tao Theorem
• Feit-Thompson Theorem
• Fundamental Theorem of Galois Theory
• Heine-Borel Theorem
• Hessenberg's Theorem = "Pappus → Desargues"
• Hilbert Basis Theorem
• Hilbert Nullstellensatz
• Hilbert-Waring theorem
• Invariance of Dimension
• IP=PSPACE
• Jordan Curve Theorem
• Kepler Conjecture
• Lie's work relating Algebras and Groups
• Nash's Theorem
• Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
• Poincaré Conjecture
• Riemann Mapping Theorem
• sorting takes Θ(N log N) steps
• Stoke's Theorem
• Stone-Weierstrass Theorem
• Thales' Theorem
• Yoneda lemma
• ζ(-1) = -1 ⁄ 12

(last modification 2018-10-24)