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
91%
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
- HOL Light, John Harrison: statement
- Mizar, Freek Wiedijk: statement
- Coq, contrib, many versions: statement
- Isabelle, Markus Wenzel: statement
- Metamath, Norman Megill: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- PVS, Bart Jacobs & John Rushby
- NuPRL, Stuart Allen, Paul Jackson
- Fundamental Theorem of Algebra
- The Denumerability of the Rational Numbers
- HOL Light, John Harrison: statement
- Mizar, Grzegorz Bancerek: statement
- Coq, contrib, Yves Bertot & Milad Niqui: statement
- Isabelle, Stefan Richter & Benjamin Porter: statement
- Metamath, revised by Mario Carneiro: statement
- ProofPower, Rob Arthan: statement
- NuPRL, Stuart Allen
- Pythagorean Theorem
- Prime Number Theorem
- Gödel's Incompleteness Theorem
- HOL Light, John Harrison: statement
- Coq, contrib, Russell O'Connor: statement
- Isabelle, Larry Paulson: statement
- nqthm, Natarajan Shankar
- Law of Quadratic Reciprocity
- HOL Light, John Harrison: statement
- Mizar, Li Yan & Xiquan Liang & Junjie Zhao: statement
- Coq, Nathanaël Courant: statement
- Isabelle, Jeremy Avigad et al.: statement
- nqthm, David Russinoff
- The Impossibility of Trisecting the Angle and Doubling the Cube
- The Area of a Circle
- Euler's Generalization of Fermat's Little Theorem
- HOL Light, John Harrison: statement
- Mizar, Yoshinori Fujisawa & Yasushi Fuwa & Hidetaka Shimizu: statement
- Coq, contrib, Laurent Théry: statement
- Isabelle, Thomas M. Rasmussen, Amine Chaieb: statement
- Metamath, Mario Carneiro: statement
- The Infinitude of Primes
- HOL Light, John Harrison: statement
- Mizar, Rafal Kwiatek: statement
- Coq, not in contribs, Russell O'Connor: statement
- Isabelle, Jacques D. Fleuriot: statement
- ProofPower, Rob Arthan: statement
- ACL2, David Russinoff
- Metamath, Norman Megill: statement
- PVS, NASA library, Ricky Butler
- The Independence of the Parallel Postulate
- Polyhedron Formula
- Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....
- Fundamental Theorem of Integral Calculus
- HOL Light, John Harrison: statement
- Mizar, Noboru Endou & Katsumi Wasaki & Yasunari Shidama: statement
- Coq, C-CoRN, Luís Cruz-Filipe: statement
- Isabelle, Jacques D. Fleuriot: statement
- Metamath, Mario Carneiro: statement
- ProofPower, Rob Arthan: statement
- ACL2, Matt Kaufmann
- PVS, NASA library, Ricky Butler
- Insolvability of General Higher Degree Equations
- De Moivre's Theorem
- Liouville's Theorem and the Construction of Transcendental Numbers
- Four Squares Theorem
- All Primes (1 mod 4) Equal the Sum of Two Squares
- Green's Theorem
- The Non-Denumerability of the Continuum
- Formula for Pythagorean Triples
- The Undecidability of the Continuum Hypothesis
- Schroeder-Bernstein Theorem
- Leibniz's Series for Pi
- HOL Light, John Harrison: statement
- Coq, standard library & C-CoRN, Luís Cruz-Filipe: statement
- Isabelle, Johannes Hoelzl: statement
- Metamath, Mario Carneiro: statement
- PVS, NASA library, David Lester
- Sum of the Angles of a Triangle
- HOL Light, John Harrison: statement
- Mizar, Wenpai Chang, Yatsuka Nakamura & Piotr Rudnicki: statement
- Coq, contrib, Frédérique Guilhot: statement
- Metamath, Mario Carneiro: statement
- Pascal's Hexagon Theorem
- Feuerbach's Theorem
- The Ballot Problem
- Ramsey's Theorem
- HOL Light, John Harrison: statement
- Mizar, Marco Riccardi: statement
- Coq, Jean-Marie Madiot: statement
- Isabelle, Tom Ridge: statement
- ProofPower, Rob Arthan & Roger Bishop Jones: statement
- PVS, NASA library, Natarajan Shankar
- nqthm, Matt Kaufmann
- NuPRL, David Basin
- The Four Color Problem
- Coq, not in contribs, Georges Gonthier: statement
- Fermat's Last Theorem
- Divergence of the Harmonic Series
- Taylor's Theorem
- HOL Light, John Harrison: statement
- Mizar, Yasunari Shidama: statement
- Coq, C-CoRN, Luís Cruz-Filipe: statement
- Isabelle, Jacques D. Fleuriot & Lukas Bulwahn & Bernhard Häupler: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa & Brittany Middleton & Jun Sawada
- PVS, NASA library, Ricky Butler
- Brouwer Fixed Point Theorem
- The Solution of a Cubic
- Arithmetic Mean/Geometric Mean
- Solutions to Pell's Equation
- Minkowski's Fundamental Theorem
- Puiseux's Theorem
- Coq, not yet in contrib, Daniel de Rauglaudre: statement
- Sum of the Reciprocals of the Triangular Numbers
- The Isoperimetric Theorem
- The Binomial Theorem
- HOL Light, John Harrison: statement
- Mizar, Christoph Schwarzweller: statement
- Coq, contrib, Laurent Théry: statement
- Isabelle, Tobias Nipkow: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- Metamath, Norman Megill: 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
- HOL Light, John Harrison: statement
- Coq, contrib, Sidi Ould Biha: statement
- Isabelle, Stephan Adelsberger, Stefan Hetzl & Florian Pollak: statement
- The Number of Platonic Solids
- Wilson's Theorem
- The Number of Subsets of a Set
- Pi is Transcendental
- Coq, Sophie Bernard & Laurence Rideau: statement
- 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
- Theorem of Ceva
- Fair Games Theorem
- Cantor's Theorem
- L'Hôpital's Rule
- Isosceles Triangle Theorem
- Sum of a Geometric Series
- HOL Light, John Harrison: statements
- Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement
- Coq, C-CoRN, Luís Cruz-Filipe: statement
- Isabelle, Jacques D. Fleuriot: statements
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- Metamath, Norman Megill: statement
- PVS, NASA library, Ricky Butler
- e is Transcendental
- Sum of an arithmetic series
- Greatest Common Divisor Algorithm
- The Perfect Number Theorem
- Order of a Subgroup
- HOL Light, John Harrison: statement
- Mizar, Wojciech Trybulec: statement
- Coq, almost C-CoRN, Dan Synek & contrib, Laurent Théry: statement
- Isabelle, Florian Kammüller: statement
- Metamath, Mario Carneiro: statement
- 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
- HOL Light, John Harrison: statement
- Mizar, Jaroslaw Kotowicz & Konrad Raczkowski & Pawel Sadowski: statement
- Coq, C-CoRN, Luís Cruz-Filipe: statement
- Isabelle, Jacques D. Fleuriot: statement
- Metamath, Mario Carneiro: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- PVS, NASA library, Bruno Dutertre
- Fourier Series
- Sum of kth powers
- The Cauchy-Schwarz Inequality
- The Intermediate Value Theorem
- HOL Light, John Harrison: statement
- Mizar, Yatsuka Nakamura & Andrzej Trybulec: statement
- Coq, C-CoRN, Herman Geuvers et al.: statement
- Isabelle, Jacques D. Fleuriot: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- Metamath, Paul Chapman: statement
- PVS, NASA library, Bruno Dutertre
- The Fundamental Theorem of Arithmetic
- HOL Light, John Harrison: statement
- Mizar, Artur Korniłowicz, Piotr Rudnicki & Hiroyuki Okazaki, Yasunari Shidama: statements
- Coq, contrib, Martijn Oostdijk: statement
- Isabelle, Thomas M. Rasmussen: statement
- ProofPower, Rob Arthan: statement
- ACL2, John Cowles
- Metamath, Paul Chapman: 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
- Desargues's Theorem
- HOL Light, John Harrison: statement
- Mizar, Wojciech Leonczuk & Krzysztof Prazmowski: statement
- Coq, contrib, Frédérique Guilhot, Julien Narboux: statement
- Metamath, Norman Megill: statement
- Derangements Formula
- The Factor and Remainder Theorems
- Stirling's Formula
- The Triangle Inequality
- HOL Light, John Harrison: statement
- Mizar, Czeslaw Bylinski: statement
- Coq, Frédérique Guilhot: statement
- Isabelle, Steven Obua: statement
- ProofPower, Rob Arthan: statement
- ACL2, Ruben Gamboa
- Metamath, Norman Megill: statement
- PVS, NASA library, Ricky Butler & Cesar Munoz
- Pick's Theorem
- The Birthday Problem
- The Law of Cosines
- HOL Light, John Harrison: statement
- Mizar, Marco Riccardi: statement
- Coq, contrib, Frédérique Guilhot: statement
- PVS, NASA library, Cesar Munoz & Ricky Butler
- 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
- 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 2015-04-16)