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

HOL Light 86 Isabelle 81 Metamath 70 Coq 69 Mizar 69 ProofPower 43 nqthm/ACL2 18 PVS 16 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

The Irrationality of the Square Root of 2 HOL Light, John Harrison: statement

Isabelle, Markus Wenzel: statement

Metamath, Norman Megill: statement

Coq, contrib, many versions: statement

Mizar, Freek Wiedijk: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

PVS, Bart Jacobs & John Rushby

NuPRL, Stuart Allen, Paul Jackson Fundamental Theorem of Algebra HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Mario Carneiro: statement

Coq, C-CoRN, Herman Geuvers et al.: statement

Mizar, Robert Milewski: statement

ProofPower, Rob Arthan: statement The Denumerability of the Rational Numbers HOL Light, John Harrison: statement

Isabelle, Stefan Richter & Benjamin Porter: statement

Metamath, revised by Mario Carneiro: statement

Coq, contrib, Yves Bertot & Milad Niqui: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement

NuPRL, Stuart Allen Pythagorean Theorem HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Norman Megill: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Akihiro Kubo & Yatsuka Nakamura: statement

ProofPower, Rob Arthan: statement

PVS, NASA library, David Lester Prime Number Theorem HOL Light, John Harrison: statement

Isabelle, Jeremy Avigad et al.: statement

Metamath, Mario Carneiro: statement Gödel's Incompleteness Theorem HOL Light, John Harrison: statement

Isabelle, Larry Paulson: statement

Coq, contrib, Russell O'Connor: statement

nqthm, Natarajan Shankar Law of Quadratic Reciprocity HOL Light, John Harrison: statement

Isabelle, Jeremy Avigad et al.: statement

Metamath, Mario Carneiro: statement

Coq, Nathanaël Courant: statement

Mizar, Li Yan & Xiquan Liang & Junjie Zhao: statement

nqthm, David Russinoff The Impossibility of Trisecting the Angle and Doubling the Cube HOL Light, John Harrison: statements

Isabelle, Ralph Romanos & Lawrence Paulson: statement The Area of a Circle HOL Light, John Harrison: statements

Isabelle, Manuel Eberl: statement

Metamath, Brendan Leahy: statement

ProofPower, Rob Arthan: statement Euler's Generalization of Fermat's Little Theorem HOL Light, John Harrison: statement

Isabelle, Thomas M. Rasmussen, Amine Chaieb: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry: statement

Mizar, Yoshinori Fujisawa & Yasushi Fuwa & Hidetaka Shimizu: statement The Infinitude of Primes HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot: statement

Metamath, Norman Megill: statement

Coq, not in contribs, Russell O'Connor: statement

Mizar, Rafal Kwiatek: statement

ProofPower, Rob Arthan: statement

ACL2, David Russinoff

PVS, NASA library, Ricky Butler The Independence of the Parallel Postulate HOL Light, John Harrison: statement

Isabelle, Tim Makarios: statement Polyhedron Formula HOL Light, John Harrison: statement

Coq, contrib, Jean-François Dufourd: statement

Mizar, Jesse Alama: statement Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + .... HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Mario Carneiro: statement

Coq, not in contribs, Jean-Marie Madiot: statement

Mizar, Karol Pak & Artur Kornilowicz: statement Fundamental Theorem of Integral Calculus HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot: statement

Metamath, Mario Carneiro: statement

Coq, C-CoRN, Luís Cruz-Filipe: statement

Mizar, Noboru Endou & Katsumi Wasaki & Yasunari Shidama: statement

ProofPower, Rob Arthan: statement

ACL2, Matt Kaufmann

PVS, NASA library, Ricky Butler Insolvability of General Higher Degree Equations De Moivre's Theorem HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot: statements

Metamath, Steve Rodriguez: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Takashi Mitsuishi & Noboru Endou & Keiji Ohkubo: statement

ProofPower, Rob Arthan: statement Liouville's Theorem and the Construction of Transcendental Numbers HOL Light, John Harrison: statements

Isabelle, Manuel Eberl: statement

Metamath, Stefan O'Rear: statement

Coq, C-CoRN, Valentin Blot: statement

Mizar, Artur Kornilowicz, Adam Naumowicz & Adam Grabowski: statement Four Squares Theorem HOL Light, John Harrison: statement

Isabelle, Roelof Oosterhuis: statement

Metamath, Mario Carneiro: statement

Coq, Guillaume Allais & Jean-Marie Madiot: statement

Mizar, Yasushige Watase: statement All Primes (1 mod 4) Equal the Sum of Two Squares HOL Light, John Harrison: statement

Isabelle, Roelof Oosterhuis: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry: statement

Mizar, Marco Riccardi: statement

ProofPower, Rob Arthan: statement Green's Theorem Isabelle, Mohammad Abdulaziz & Lawrence Paulson: statement The Non-Denumerability of the Continuum HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Norman Megill: statement

Coq, C-CoRN: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement Formula for Pythagorean Triples HOL Light, John Harrison: statement

Isabelle, Roelof Oosterhuis: statement

Metamath, Scott Fenton: statement

Coq, contrib, David Delahaye: statement

Mizar, Freek Wiedijk: statement

ProofPower, Rob Arthan: statement The Undecidability of the Continuum Hypothesis Schroeder-Bernstein Theorem HOL Light, John Harrison: statement

Isabelle, Tobias Nipkow: statement

Metamath, Norman Megill: statement

Coq, contrib, Hugo Herbelin: statement

Mizar, Piotr Rudnicki & Andrzej Trybulec: statement

ProofPower, Rob Arthan: statement Leibniz's Series for Pi HOL Light, John Harrison: statement

Isabelle, Johannes Hoelzl: statement

Metamath, Mario Carneiro: statement

Coq, standard library & C-CoRN, Luís Cruz-Filipe: statement

Mizar, Karol Pak: statement

PVS, NASA library, David Lester Sum of the Angles of a Triangle HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Wenpai Chang, Yatsuka Nakamura & Piotr Rudnicki: statement Pascal's Hexagon Theorem HOL Light, John Harrison: statement

Coq, Nicolas Magaud & Julien Narboux: statement

Mizar, Roland Coghetto: statement Feuerbach's Theorem HOL Light, John Harrison: statement

Coq, not in contribs, CertiGeo team: statement The Ballot Problem HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Thierry Arnoux: statement

Coq, Jean-Marie Madiot: statement

Mizar, Karol Pak: statement

ProofPower, Rob Arthan: statement Ramsey's Theorem HOL Light, John Harrison: statement

Isabelle, Tom Ridge: statement

Metamath, Mario Carneiro: statement

Coq, Jean-Marie Madiot: statement

Mizar, Marco Riccardi: 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 HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement

ProofPower, Rob Arthan: statement Taylor's Theorem HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot & Lukas Bulwahn & Bernhard Häupler: statement

Metamath, Mario Carneiro: statement

Coq, C-CoRN, Luís Cruz-Filipe: statement

Mizar, Yasunari Shidama: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa & Brittany Middleton & Jun Sawada

PVS, NASA library, Ricky Butler Brouwer Fixed Point Theorem HOL Light, John Harrison: statement

Isabelle, Robert Himmelmann: statement

Mizar, Karol Pak: statement The Solution of a Cubic HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Mario Carneiro: statement

Mizar, Marco Riccardi: statement Arithmetic Mean/Geometric Mean HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Mario Carneiro: statement

Coq, not in contribs, Jean-Marie Madiot: statement

Mizar, Adam Grabowski: statement

ProofPower, Rob Arthan: statement

ACL2, Matt Kaufmann, Paolo Pecchiari Solutions to Pell's Equation HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Stefan O'Rear: statement

Mizar, Marcin Acewicz & Karol Pak: statement Minkowski's Fundamental Theorem HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

ProofPower, Rob Arthan: statement Puiseux's Theorem Coq, not yet in contrib, Daniel de Rauglaudre: statement Sum of the Reciprocals of the Triangular Numbers HOL Light, John Harrison: statement

Isabelle, Iain Whiteside: statement

Metamath, Scott Fenton: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Adam Grabowski: statement

ProofPower, Rob Arthan: statement The Isoperimetric Theorem The Binomial Theorem HOL Light, John Harrison: statement

Isabelle, Tobias Nipkow: statement

Metamath, Norman Megill: statement

Coq, contrib, Laurent Théry: statement

Mizar, Christoph Schwarzweller: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

NuPRL, Paul Jackson & Rich Eaton The Partition Theorem HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Thierry Arnoux: statement

Mizar, Karol Pak: statement The Solution of the General Quartic Equation HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Mario Carneiro: statement

Mizar, Marco Riccardi: statement The Central Limit Theorem Isabelle, Jeremy Avigad: statement Dirichlet's Theorem HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Mario Carneiro: statement The Cayley-Hamilton Theorem HOL Light, John Harrison: statement

Isabelle, Stephan Adelsberger, Stefan Hetzl & Florian Pollak: statement

Coq, contrib, Sidi Ould Biha: statement The Number of Platonic Solids HOL Light, John Harrison: statement Wilson's Theorem HOL Light, John Harrison: statement

Isabelle, Thomas M. Rasmussen: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry: statement

Mizar, Marco Riccardi: statement

ProofPower, Rob Arthan: statement

nqthm, David Russinoff The Number of Subsets of a Set HOL Light, John Harrison: statement

Isabelle, Florian Kammüller: statement

Metamath, Norman Megill: statement

Coq, contrib, Laurent Théry: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement Pi is Transcendental Isabelle, Manuel Eberl: statement

Coq, Sophie Bernard & Laurence Rideau: statement Konigsberg Bridges Problem HOL Light, John Harrison: statement

Isabelle, Wenda Li: statement

Metamath, Mario Carneiro: statement

Coq, Jean-Marie Madiot: statement

Mizar, Adam Naumowicz: statement Product of Segments of Chords HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, David Moews: statement

Coq, not in contribs, Loïc Pottier: statement

Mizar, Marco Riccardi: statement The Hermite-Lindemann Transcendence Theorem Coq, Sophie Bernard: statement Heron's Formula HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Marco Riccardi: statement Formula for the Number of Combinations HOL Light, John Harrison: statement

Isabelle, Larry Paulson: statement

Metamath, Mario Carneiro: statement

Coq, Pierre Letouzey: statement

Mizar, Karol Pak: statement

ProofPower, Rob Arthan: statement The Laws of Large Numbers Bezout's Theorem HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Mario Carneiro: statement

Coq, standard library: statement

Mizar, Rafal Kwiatek: statement

ProofPower, Rob Arthan: statement

ACL2, John Cowles

NuPRL, Paul Jackson & Mark Bickford Theorem of Ceva HOL Light, John Harrison: statement

Metamath, Saveliy Skresanov: statement

Coq, contrib, Frédérique Guilhot, Julien Narboux: statement

Mizar, Boris A. Shminke: statement Fair Games Theorem Cantor's Theorem HOL Light, John Harrison: statement

Isabelle, Larry Paulson: statement

Metamath, Norman Megill: statement

Coq, Jorik Mandemaker: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement

NuPRL, Jim Caldwell L'Hôpital's Rule HOL Light, John Harrison: statement

Isabelle, Johannes Hölzl: statement

Metamath, Mario Carneiro: statement

Coq, Sylvain Dailler: statement

Mizar, Malgorzata Korolkiewicz: statement

ProofPower, Rob Arthan: statement Isosceles Triangle Theorem HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Saveliy Skresanov: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Marco Riccardi: statement Sum of a Geometric Series HOL Light, John Harrison: statements

Isabelle, Jacques D. Fleuriot: statements

Metamath, Norman Megill: statement

Coq, C-CoRN, Luís Cruz-Filipe: statement

Mizar, Konrad Raczkowski & Andrzej Nedzusiak: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

PVS, NASA library, Ricky Butler e is Transcendental HOL Light, Jesse Bingham: statement

Isabelle, Manuel Eberl: statement

Coq, Sophie Bernard & Laurence Rideau: statement Sum of an arithmetic series HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Norman Megill: statement

Coq, not in contribs, many versions: statement

Mizar, Ming Liang & Yuzhong Ding: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa Greatest Common Divisor Algorithm HOL Light, John Harrison: statements

Isabelle, Larry Paulson: statement

Metamath, Paul Chapman: statement

Coq, standard library: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement

ACL2, David Russinoff

NuPRL, Paul Jackson & Rich Eaton The Perfect Number Theorem HOL Light, John Harrison: statement

Isabelle, Mark IJbema: statement

Metamath, Mario Carneiro: statement

Mizar, Marco Riccardi: statement Order of a Subgroup HOL Light, John Harrison: statement

Isabelle, Florian Kammüller: statement

Metamath, Mario Carneiro: statement

Coq, almost C-CoRN, Dan Synek & contrib, Laurent Théry: statement

Mizar, Wojciech Trybulec: statement

ProofPower, Rob Arthan: statement

PVS, NASA library, David Lester Sylow's Theorem HOL Light, Alexey Solovyev: statement

Isabelle, Florian Kammüller: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry: statement

Mizar, Marco Riccardi: statements

PVS, André Galdino Ascending or Descending Sequences HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Mario Carneiro: statement

Coq, Florent Hivert: statement

Mizar, Piotr Rudnicki: statements The Principle of Mathematical Induction HOL Light, John Harrison: statement

Isabelle, Tobias Nipkow: statement

Metamath, Raph Levien: statement

Coq, standard library: statement

Mizar, Grzegorz Bancerek: statement

ProofPower, Rob Arthan: statement The Mean Value Theorem HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot: statement

Metamath, Mario Carneiro: statement

Coq, C-CoRN, Luís Cruz-Filipe: statement

Mizar, Jaroslaw Kotowicz & Konrad Raczkowski & Pawel Sadowski: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

PVS, NASA library, Bruno Dutertre Fourier Series HOL Light, John Harrison: statement Sum of kth powers HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Scott Fenton: statement The Cauchy-Schwarz Inequality HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Norman Megill: statement

Coq, Daniel de Rauglaudre: statement

Mizar, Jaroslaw Kotowicz: statement

ProofPower, Rob Arthan: statement

PVS, NASA library, Ricky Butler The Intermediate Value Theorem HOL Light, John Harrison: statement

Isabelle, Jacques D. Fleuriot: statement

Metamath, Paul Chapman: statement

Coq, C-CoRN, Herman Geuvers et al.: statement

Mizar, Yatsuka Nakamura & Andrzej Trybulec: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

PVS, NASA library, Bruno Dutertre The Fundamental Theorem of Arithmetic HOL Light, John Harrison: statement

Isabelle, Thomas M. Rasmussen: statement

Metamath, Paul Chapman: statement

Coq, contrib, Martijn Oostdijk: statement

Mizar, Artur Korniłowicz, Piotr Rudnicki & Hiroyuki Okazaki, Yasunari Shidama: statements

ProofPower, Rob Arthan: statement

ACL2, John Cowles

PVS, NASA library, Ricky Butler

NuPRL, Stuart Allen & Paul Jackson Divergence of the Prime Reciprocal Series HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, Mario Carneiro: statement

ProofPower, Rob Arthan: statement Dissection of Cubes (J.E. Littlewood's "elegant" proof) The Friendship Theorem HOL Light, John Harrison: statement

Isabelle, Wenda Li: statement

Metamath, Alexander van der Vekens: statement

Mizar, Karol Pak: statement Morley's Theorem HOL Light, John Harrison: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Roland Coghetto: statement Divisibility by 3 Rule HOL Light, John Harrison: statement

Isabelle, Benjamin Porter: statement

Metamath, Mario Carneiro: statement

Coq, standard library: statement

Mizar, Adam Naumowicz: statement

ProofPower, Rob Arthan: statement Lebesgue Measure and Integration HOL Light, John Harrison: statement

Isabelle, Stefan Richter: statement

Metamath, Mario Carneiro: statement

Mizar, Noboru Endou & Yasunari Shidama: statement Desargues's Theorem HOL Light, John Harrison: statement

Metamath, Norman Megill: statement

Coq, contrib, Frédérique Guilhot, Julien Narboux: statement

Mizar, Wojciech Leonczuk & Krzysztof Prazmowski: statement Derangements Formula HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Mario Carneiro: statement

Mizar, Cezary Kaliszyk: statement The Factor and Remainder Theorems HOL Light, John Harrison: statement

Isabelle, Clemens Ballarin: statements

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry, Loïc Pottier: statement

Mizar, Piotr Rudnicki: statement

ProofPower, Rob Arthan: statement Stirling's Formula HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statements

Metamath, Glauco Siliprandi: statement

Coq, not in contribs, Coqtail team: statement The Triangle Inequality HOL Light, John Harrison: statement

Isabelle, Steven Obua: statement

Metamath, Norman Megill: statement

Coq, Frédérique Guilhot: statement

Mizar, Czeslaw Bylinski: statement

ProofPower, Rob Arthan: statement

ACL2, Ruben Gamboa

PVS, NASA library, Ricky Butler & Cesar Munoz Pick's Theorem HOL Light, John Harrison: statement The Birthday Problem HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, Mario Carneiro: statement

Coq, Jean-Marie Madiot: statement

Mizar, Cezary Kaliszyk: statement

ProofPower, Rob Arthan: statement The Law of Cosines HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

Metamath, David A. Wheeler: statement

Coq, contrib, Frédérique Guilhot: statement

Mizar, Marco Riccardi: statement

PVS, NASA library, Cesar Munoz & Ricky Butler Ptolemy's Theorem HOL Light, John Harrison: statement

Isabelle, Lukas Bulwahn: statement

Metamath, David A. Wheeler: statement

Coq, Tuan Minh Pham: statement

Mizar, Marco Riccardi: statement Principle of Inclusion/Exclusion HOL Light, John Harrison: statement

Isabelle, Andreas Lochbihler: statement

Metamath, Mario Carneiro: statement

Coq, Jean-Marie Madiot: statement

Mizar, Karol Pak: statement

ProofPower, Rob Arthan: statement Cramer's Rule HOL Light, John Harrison: statement

Isabelle, Amine Chaieb: statement

Metamath, Alexander van der Vekens (building on work by Stefan O'Rear): statement

Coq, not in contribs, Georges Gonthier et al.: statement

Mizar, Karol Pak: statement Bertrand's Postulate HOL Light, John Harrison: statement

Isabelle, Julian Biendarra & Manuel Eberl: statement

Metamath, Mario Carneiro: statement

Coq, contrib, Laurent Théry: statement

Mizar, Marco Riccardi: statement Buffon Needle Problem Isabelle, Manuel Eberl: statement

ProofPower, Rob Arthan: statement Descartes Rule of Signs HOL Light, John Harrison: statement

Isabelle, Manuel Eberl: statement

ProofPower, Rob Arthan: statement

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"

= "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

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