Freek Wiedijk maintains a list of 100 well-known math theorems and tracks which of them have been formalized. As of May 2014, all but 11 had been formalized. There is a wiki page of 27 notoriously long mathematical proofs. Only three of them have been formalized: Feit-Thompson’s odd order theorem, the four-color theorem, and the Kepler conjecture. Merging lists, we obtain the following list of suggestions for formal proof projects.

- Insolvability of General Higher Degree Equations (Abel-Ruffini)
- Green’s theorem
- The undecidability of the Continuum Hypothesis
- Fermat’s Last theorem
- Puiseux’s Theorem
- The Isoperimetric Inequality
- The Hermite-Lindemann Transcendence Theorem
- The Law of Large Numbers
- Dissection of Cubes (Littlewood)
- Classification of simple complex Lie algebras
- Constructibility of the 65537-gon
- Lasker-Noether theorem
- Resolution of singularities in characteristic zero
- Resolution of singularities for 3-folds in characteristic at least 7 (Abyhankar)
- Discrete series representations of Lie groups (Harish-Chandra)
- Burnside’s bounded exponent problem (negative solution by Novikov-Adian)
- Grothendieck’s FGA and SGA
- Ramanujan conjecture and the Weil conjectures
- Eisenstein series (Langlands)
- Arthur-Selberg trace formula
- Almgren’s regularity theorem
- Lafforgue’s theorem
- Poincare conjecture
- Thurston’s geometrization conjecture
- Classification of finite simple groups
- Robertson-Seymour theorem
- Strong perfect graph theorem

Advertisements