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):
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
- 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
- Naproche, Peter Koepke, Mateusz Marcol & Patrick Schäfer
- NuPRL, Stuart Allen, Paul Jackson
- Fundamental Theorem of Algebra
- Isabelle, Amine Chaieb: statement
- HOL Light, John Harrison: statement
- Coq, C-CoRN, Herman Geuvers et al.: statement
- Lean, Chris Hughes: statement
- Metamath, Mario Carneiro: statement
- Mizar, Robert Milewski: statement
- ACL2, Ruben Gamboa & John Cowles
- ProofPower, Rob Arthan: statement
- PVS, Anthony Narkawicz
- 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
- NuPRL, Stuart Allen
- Pythagorean Theorem
- Isabelle, Amine Chaieb: statement
- HOL Light, John Harrison: statement
- Coq, contrib, Frédérique Guilhot: statement
- Lean, Joseph Myers: statement
- Metamath, Norman Megill: statement
- Mizar, Akihiro Kubo & Yatsuka Nakamura: statement
- ProofPower, Rob Arthan: statement
- PVS, NASA library, David Lester
- Prime Number Theorem
- Gödel's Incompleteness Theorem
- Isabelle, Larry Paulson: statement
- HOL Light, John Harrison: statement
- Coq, contrib, Russell O'Connor: statement
- nqthm, Natarajan Shankar
- Law of Quadratic Reciprocity
- The Impossibility of Trisecting the Angle and Doubling the Cube
- 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
- 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
- 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
- Naproche, Peter Koepke
- The Independence of the Parallel Postulate
- Polyhedron Formula
- Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
- 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
- Insolvability of General Higher Degree Equations
- Coq, Sophie Bernard & Cyril Cohen & Assia Mahboubi & Pierre-Yves Strub, statement
- Lean, Thomas Browning: statement
- De Moivre's Theorem
- Liouville's Theorem and the Construction of Transcendental Numbers
- 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
- All Primes (1 mod 4) Equal the Sum of Two Squares
- Isabelle, Roelof Oosterhuis: statement
- HOL Light, John Harrison: statement
- Coq, contrib, Laurent Théry: statement
- Lean, Chris Hughes: statement
- Metamath, Mario Carneiro: statement
- Mizar, Marco Riccardi: statement
- ACL2, David M. Russinoff
- ProofPower, Rob Arthan: statement
- PVS, Anthony Narkawicz
- Green's Theorem
- Isabelle, Mohammad Abdulaziz & Larry Paulson: statement
- The Non-Denumerability of the Continuum
- Formula for Pythagorean Triples
- 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
- 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
- ProofPower, Rob Arthan: statement
- Naproche, Peter Koepke & Marcel Schütz
- Leibniz's Series for Pi
- Sum of the Angles of a Triangle
- Pascal's Hexagon Theorem
- Feuerbach's Theorem
- The Ballot Problem
- Ramsey's Theorem
- Isabelle, Tom Ridge: statement
- HOL Light, John Harrison: statement
- Coq, Frédéric Blanqui: statement
- Lean, Bhavik Mehta: statement
- Metamath, Mario Carneiro: statement
- Mizar, Marco Riccardi: statement
- ProofPower, Rob Arthan & Roger Bishop Jones: statement
- nqthm, Matt Kaufmann
- PVS, NASA library, Natarajan Shankar
- NuPRL, David Basin
- The Four Color Problem
- Coq, not in contribs, Georges Gonthier: statement
- Fermat's Last Theorem
- 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
- 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
- Brouwer Fixed Point Theorem
- The Solution of a Cubic
- Arithmetic Mean/Geometric Mean
- Isabelle, Benjamin Porter: statement
- HOL Light, John Harrison: statement
- Coq, not in contribs, Jean-Marie Madiot: statement
- Lean, Yury G. Kudryashov: statement
- Metamath, Mario Carneiro: statement
- Mizar, Adam Grabowski: statement
- ACL2, Matt Kaufmann, Paolo Pecchiari
- ProofPower, Rob Arthan: statement
- Solutions to Pell's Equation
- Minkowski's Fundamental Theorem
- Puiseux's Theorem
- Isabelle, Manuel Eberl: statement
- Coq, not yet in contrib, Daniel de Rauglaudre: statement
- Sum of the Reciprocals of the Triangular Numbers
- The Isoperimetric Theorem
- The Binomial Theorem
- Isabelle, Tobias Nipkow: statement
- HOL Light, John Harrison: statement
- Coq, contrib, Laurent Théry: statement
- Lean, Chris Hughes: statement
- Metamath, Norman Megill: statement
- Mizar, Christoph Schwarzweller: statement
- ACL2, Ruben Gamboa
- ProofPower, Rob Arthan: statement
- NuPRL, Paul Jackson & Rich Eaton
- The Partition Theorem
- The Solution of the General Quartic Equation
- The Central Limit Theorem
- Dirichlet's Theorem
- 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
- The Number of Platonic Solids
- Wilson's Theorem
- The Number of Subsets of a Set
- Isabelle, Florian Kammüller: statement
- HOL Light, John Harrison: statement
- Coq, contrib, Laurent Théry: statement
- Lean, mathlib: statement
- Metamath, Norman Megill: statement
- Mizar, Grzegorz Bancerek: statement
- ACL2, David M. Russinoff
- ProofPower, Rob Arthan: statement
- Naproche, Patrick Schäfer
- Pi is Transcendental
- Konigsberg Bridges Problem
- Product of Segments of Chords
- The Hermite-Lindemann Transcendence Theorem
- Heron's Formula
- Formula for the Number of Combinations
- The Laws of Large Numbers
- Bezout's Theorem
- Isabelle, Amine Chaieb: statement
- HOL Light, John Harrison: statement
- Coq, standard library: statement
- Lean, mathlib: statement
- Metamath, Mario Carneiro: statement
- Mizar, Rafal Kwiatek: statement
- ACL2, John Cowles
- ProofPower, Rob Arthan: statement
- Naproche, Mateusz Marcol & Patrick Schäfer
- NuPRL, Paul Jackson & Mark Bickford
- Theorem of Ceva
- Fair Games Theorem
- Cantor's Theorem
- L'Hôpital's Rule
- Isosceles Triangle Theorem
- 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
- e is Transcendental
- 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
- 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
- Naproche, Mateusz Marcol & Patrick Schäfer
- The Perfect Number Theorem
- 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
- Sylow's Theorem
- Ascending or Descending Sequences
- The Principle of Mathematical Induction
- 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
- Fourier Series
- Sum of kth powers
- The Cauchy-Schwarz Inequality
- Isabelle, Benjamin Porter: statement
- HOL Light, John Harrison: statement
- Coq, Daniel de Rauglaudre: statement
- Lean, Zhouhang Zhou: statement
- Metamath, Norman Megill: statement
- Mizar, Jaroslaw Kotowicz: statement
- ACL2, Carl Kwan
- ProofPower, Rob Arthan: statement
- PVS, NASA library, Ricky Butler
- 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
- 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
- NuPRL, Stuart Allen & Paul Jackson
- Divergence of the Prime Reciprocal Series
- Dissection of Cubes (J.E. Littlewood's "elegant" proof)
- The Friendship Theorem
- Morley's Theorem
- Divisibility by 3 Rule
- 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
- Desargues's Theorem
- Derangements Formula
- The Factor and Remainder Theorems
- 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
- The Triangle Inequality
- Isabelle, Steven Obua: statement
- HOL Light, John Harrison: statement
- Coq, Frédérique Guilhot: statement
- Lean, Zhouhang Zhou: statement
- Metamath, Norman Megill: statement
- Mizar, Czeslaw Bylinski: statement
- ACL2, Ruben Gamboa
- ProofPower, Rob Arthan: statement
- PVS, NASA library, Ricky Butler & Cesar Munoz
- Pick's Theorem
- The Birthday Problem
- The Law of Cosines
- Ptolemy's Theorem
- Principle of Inclusion/Exclusion
- Cramer's Rule
- Bertrand's Postulate
- Buffon Needle Problem
- 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
- Cantor-Bendixson 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
- The Fundamental Theorem of Finite Abelian Groups
- 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
- Stokes' Theorem
- Stone-Weierstrass Theorem
- Thales' Theorem
- Thue-Siegel-Roth theorem about approximating algebraic numbers by rationals
- Yoneda lemma
- ζ(-1) = -1 ⁄ 12
- existence of ZF+DC+IHC model in which all real subsets are Lebesque measurable, have the perfect set property, and are Baire
(last modification 2023-10-24)