A redesign of someone else's page

Formalizing 100 Theorems

Since 1999 there has been a list of the "top 100" mathematical theorems on the web. Freek Wiedijk keeps track of which of them have been proved in a machine-checked proof assistant, and thirteen communities of mathematicians and computer scientists have been working through it ever since. 99 of the hundred are done.

This site is not his. It is a redesign of his page — the same data, the same credits, the same links out — rearranged so you can see the shape of it. His page presents a hundred theorems by thirteen systems as a single column 538 pixels wide; the data is a grid, so this shows it as one.

The list

Theorems down, systems across, in his numbering and his column order. A mark means that system has a proof of that theorem, and most marks link to the statement on that system's own list of the hundred — the same links his page carries. Every row is anchored by its number, so this goes straight to #33, exactly as it does on his.

●: Formalized
◆: Formalized, with a constructive proof — 45 of them
·: Not formalized in that system
difficult: One of the 6 he marks as a serious challenge

All 100 theorems by the 13 proof assistants that track them, in his numbering and his column order — systems by how much of the list each has covered, highest first.
Theorem	HOL Light95	Isabelle92	Lean82	Rocq80	Metamath74	Mizar71	nqthm/ACL248	ProofPower43	PVS26	Imandra20	Megalodon12	Naproche10	NuPRL/MetaPRL8	Systems
1 The Irrationality of the Square Root of 2														13of 13 systems
2 Fundamental Theorem of Algebra														9of 13 systems
3 The Denumerability of the Rational Numbers														12of 13 systems
4 Pythagorean Theorem														9of 13 systems
5 Prime Number Theorem														4of 13 systems
6 Gödel's Incompleteness Theorem														5of 13 systems
7 Law of Quadratic Reciprocity														7of 13 systems
8 The Impossibility of Trisecting the Angle and Doubling the Cube														2of 13 systems
9 The Area of a Circle														6of 13 systems
10 Euler's Generalization of Fermat's Little Theorem														7of 13 systems
11 The Infinitude of Primes														12of 13 systems
12 The Independence of the Parallel Postulate														2of 13 systems
13 Polyhedron Formula														4of 13 systems
14 Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ....														6of 13 systems
15 Fundamental Theorem of Integral Calculus														9of 13 systems
16 Insolvability of General Higher Degree Equations														2of 13 systems
17 De Moivre's Theorem														8of 13 systems
18 Liouville's Theorem and the Construction of Transcendental Numbers														6of 13 systems
19 Four Squares Theorem														8of 13 systems
20 All Primes (1 mod 4) Equal the Sum of Two Squares														9of 13 systems
21 Green's Theorem difficult														2of 13 systems
22 The Non-Denumerability of the Continuum														10of 13 systems
23 Formula for Pythagorean Triples														8of 13 systems
24 The Undecidability of the Continuum Hypothesis difficult														2of 13 systems
25 Schroeder-Bernstein Theorem														10of 13 systems
26 Leibniz's Series for Pi														7of 13 systems
27 Sum of the Angles of a Triangle														6of 13 systems
28 Pascal's Hexagon Theorem														3of 13 systems
29 Feuerbach's Theorem														2of 13 systems
30 The Ballot Problem														8of 13 systems
31 Ramsey's Theorem														11of 13 systems
32 The Four Color Problem difficult														1of 13 systems
33 Fermat's Last Theorem difficult unformalized														0of 13 systems
34 Divergence of the Harmonic Series														10of 13 systems
35 Taylor's Theorem														9of 13 systems
36 Brouwer Fixed Point Theorem														4of 13 systems
37 The Solution of a Cubic														6of 13 systems
38 Arithmetic Mean/Geometric Mean														8of 13 systems
39 Solutions to Pell's Equation														5of 13 systems
40 Minkowski's Fundamental Theorem														4of 13 systems
41 Puiseux's Theorem														2of 13 systems
42 Sum of the Reciprocals of the Triangular Numbers														9of 13 systems
43 The Isoperimetric Theorem difficult														1of 13 systems
44 The Binomial Theorem														10of 13 systems
45 The Partition Theorem														6of 13 systems
46 The Solution of the General Quartic Equation														6of 13 systems
47 The Central Limit Theorem														2of 13 systems
48 Dirichlet's Theorem difficult														4of 13 systems
49 The Cayley-Hamilton Theorem														5of 13 systems
50 The Number of Platonic Solids														1of 13 systems
51 Wilson's Theorem														8of 13 systems
52 The Number of Subsets of a Set														11of 13 systems
53 Pi is Transcendental														3of 13 systems
54 Konigsberg Bridges Problem														8of 13 systems
55 Product of Segments of Chords														6of 13 systems
56 The Hermite-Lindemann Transcendence Theorem														3of 13 systems
57 Heron's Formula														6of 13 systems
58 Formula for the Number of Combinations														9of 13 systems
59 The Laws of Large Numbers														4of 13 systems
60 Bezout's Theorem														12of 13 systems
61 Theorem of Ceva														5of 13 systems
62 Fair Games Theorem														3of 13 systems
63 Cantor's Theorem														11of 13 systems
64 L'Hôpital's Rule														7of 13 systems
65 Isosceles Triangle Theorem														7of 13 systems
66 Sum of a Geometric Series														11of 13 systems
67 e is Transcendental														6of 13 systems
68 Sum of an arithmetic series														11of 13 systems
69 Greatest Common Divisor Algorithm														13of 13 systems
70 The Perfect Number Theorem														7of 13 systems
71 Order of a Subgroup														9of 13 systems
72 Sylow's Theorem														8of 13 systems
73 Ascending or Descending Sequences														7of 13 systems
74 The Principle of Mathematical Induction														11of 13 systems
75 The Mean Value Theorem														9of 13 systems
76 Fourier Series														4of 13 systems
77 Sum of kth powers														5of 13 systems
78 The Cauchy-Schwarz Inequality														10of 13 systems
79 The Intermediate Value Theorem														9of 13 systems
80 The Fundamental Theorem of Arithmetic														12of 13 systems
81 Divergence of the Prime Reciprocal Series														8of 13 systems
82 Dissection of Cubes (J.E. Littlewood's "elegant" proof)														3of 13 systems
83 The Friendship Theorem														6of 13 systems
84 Morley's Theorem														4of 13 systems
85 Divisibility by 3 Rule														10of 13 systems
86 Lebesgue Measure and Integration														6of 13 systems
87 Desargues's Theorem														5of 13 systems
88 Derangements Formula														7of 13 systems
89 The Factor and Remainder Theorems														7of 13 systems
90 Stirling's Formula														5of 13 systems
91 The Triangle Inequality														10of 13 systems
92 Pick's Theorem														2of 13 systems
93 The Birthday Problem														8of 13 systems
94 The Law of Cosines														7of 13 systems
95 Ptolemy's Theorem														6of 13 systems
96 Principle of Inclusion/Exclusion														9of 13 systems
97 Cramer's Rule														7of 13 systems
98 Bertrand's Postulate														6of 13 systems
99 Buffon Needle Problem														4of 13 systems
100 Descartes Rule of Signs														4of 13 systems

His page carries all of this in typography — italics for unformalized, italics again for constructive, underline for difficult — explained in a paragraph far above the list, and none of it survives being read aloud. Here every mark is a shape as well as a colour, every flag is a word, and every cell names its system, its state and whoever is credited for it.

What the project records

The list of theorems is not his either, and he is careful to say so. It is "The Hundred Greatest Theorems", which Paul and Jack Abad presented at a mathematics conference in July 1999, ranked on "the place the theorem holds in the literature, the quality of the proof, and the unexpectedness of the result". He calls it "a rather arbitrary list (and most of the theorems seem rather elementary), but still is nice to look at". What he added was the tracking.

Not every formalization of these theorems is here. In his words, the page "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" — which is how the thirteen systems earned their place, and why the columns are ordered by how much of the list each has covered rather than alphabetically or by age.

As of this snapshot the record holds 661 formalizations across 13 systems. 629 of them credit the people who did the work by name, 617 link to the statement as it was actually proved, and 45 are marked as constructive proofs. That accumulation is the reason the project is worth admiring, and it is the part a redesign has to be careful not to flatten away.

What the data says once you can see it

These are the questions his page holds the answers to but cannot show you, because a single column in numeric order will not let you ask them.

99 of the 100 have been formalized. The one that has not is #33, Fermat's Last Theorem — which is where the 99% on his page comes from.
Two theorems have been done in every one of the thirteen systems: #1, The Irrationality of the Square Root of 2 and #69, Greatest Common Divisor Algorithm.
Four theorems have been done at most once: #33, Fermat's Last Theorem (0); #32, The Four Color Problem (1); #43, The Isoperimetric Theorem (1); #50, The Number of Platonic Solids (1). Three of those four are also among the 6 he marks as difficult, which is a correlation his page never puts side by side.

Every figure above is counted from a copy of his page as he last modified it on 2026-04-09, taken 2026-08-05. Nothing here is fetched at runtime, and nothing here is more current than the original. Every outbound link is his, with two exceptions: links of his that are now dead are sent where that page lives today, and /about/ says which and why.