Not on the list
What the 1999 list left out
The hundred is someone else's list from 1999, and people have been writing to him about its omissions ever since. He keeps their suggestions at the foot of his page — 41 of them, alphabetical — and 24 have been formalized anyway, even though no column on the main list is counting them.
In his words: "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.)"
On his page this list has no heading of its own — the <h2> above it is empty, used as a spacer, which is one of the three things an accessibility audit flags on the original. It has one here.
| Theorem | Formalized? |
|---|---|
| Atiyah-Singer Index Theorem | Not formalized |
| Baker's Theorem on Linear Forms in Logarithms | Not formalized |
| Black-Scholes Formula | Not formalized |
| Borsuk-Ulam Theorem | Formalized |
| Cantor-Bendixson theorem | Not formalized |
| Cauchy's Integral Theorem | Formalized |
| Cauchy's Residue Theorem | Formalized |
| Chen's theorem | Not formalized |
| every vector space is free | Formalized |
| Classification of Finite Simple Groups | Not formalized |
| Classification of semisimple Lie groups (Killing, Cartan, Dynkin) | Not formalized |
| Sophie Germain's theorem | Formalized |
| Gödel's Completeness Theorem | Formalized |
| Gödel's Second Incompleteness Theorem | Formalized |
| Green-Tao Theorem | Not formalized |
| Feit-Thompson Theorem | Formalized |
| The Fundamental Theorem of Finite Abelian Groups | Formalized |
| Fundamental Theorem of Galois Theory | Formalized |
| Heine-Borel Theorem | Formalized |
| Hessenberg's Theorem = "Pappus → Desargues" | Formalized |
| Hilbert Basis Theorem | Formalized |
| Hilbert Nullstellensatz | Formalized |
| Hilbert-Waring theorem | Not formalized |
| Invariance of Dimension | Formalized |
| IP=PSPACE | Not formalized |
| Jordan Curve Theorem | Formalized |
| Kepler Conjecture | Formalized |
| Lie's work relating Algebras and Groups | Not formalized |
| Nash's Theorem | Not formalized |
| Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds | Not formalized |
| Poincaré Conjecture | Not formalized |
| Riemann Mapping Theorem | Formalized |
| sorting takes Θ(N log N) steps | Formalized |
| Stokes' Theorem | Not formalized |
| Stone-Weierstrass Theorem | Formalized |
| Tarski-Banach | Formalized |
| Thales' Theorem | Formalized |
| Thue-Siegel-Roth theorem about approximating algebraic numbers by rationals | Not formalized |
| Yoneda lemma | Formalized |
| ζ(-1) = -1 ⁄ 12 | Formalized |
| existence of ZF+DC+IHC model in which all real subsets are Lebesque measurable, have the perfect set property, and are Baire | Not formalized |
He marks these the same way he marks the hundred, and inverted from what you might expect: bold for the ones that have been formalized, italics for the ones that have not. That is the whole legend, and it is not written down anywhere on the page. Both states are spelled out above, from a copy of his page as he last modified it on 2026-04-09.