27 Formal Proof Projects

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.

  1. Insolvability of General Higher Degree Equations (Abel-Ruffini)
  2. Green’s theorem
  3. The undecidability of the Continuum Hypothesis
  4. Fermat’s Last theorem
  5. Puiseux’s Theorem
  6. The Isoperimetric Inequality
  7. The Hermite-Lindemann Transcendence Theorem
  8. The Law of Large Numbers
  9. Dissection of Cubes (Littlewood)
  10. Classification of simple complex Lie algebras
  11. Constructibility of the 65537-gon
  12. Lasker-Noether theorem
  13. Resolution of singularities in characteristic zero
  14. Resolution of singularities for 3-folds in characteristic at least 7 (Abyhankar)
  15. Discrete series representations of Lie groups (Harish-Chandra)
  16. Burnside’s bounded exponent problem (negative solution by Novikov-Adian)
  17. Grothendieck’s FGA and SGA
  18. Ramanujan conjecture and the Weil conjectures
  19. Eisenstein series (Langlands)
  20. Arthur-Selberg trace formula
  21. Almgren’s regularity theorem
  22. Lafforgue’s theorem
  23. Poincare conjecture
  24. Thurston’s geometrization conjecture
  25. Classification of finite simple groups
  26. Robertson-Seymour theorem
  27. Strong perfect graph theorem

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s