Why haven't all of the "hundred greatest theorems" been formalized yet?

Question

The "hundred greatest theorems" used to be maintained here.

See this page for the current status of the formalization of these theorems.

Apparentely, Fermat's Last Theorem, the Isoperimetric Theorem, and the Fair Games Theorem are the only theorems on this list that have yet to be formalized.

What are the main difficulties with formalizing these theorems? Presumably, each theorem presents its own difficulties.

Answer 1

The main difficulty in formalising a proof of Fermat's Last Theorem is that all the known human proofs involve a vast amount of algebraic and analytic geometry (thousands of pages) and a vast amount of harmonic analysis (at least hundreds of pages). In theory there is no obstruction to typing all of this stuff into a computer proof system. In practice, if you want me to manage a team to do it then my estimate is a $100,000,000 grant to hire a team of people who would be happy to spend around a decade working on the project (and hence not doing other things such as generating research papers). As a consequence we would produce a fully-formalised proof, and the mathematics community would take one look at it and say "Why did you do that? We already knew it was true -- Taylor and Wiles proved it in 1995". (Remark: Taylor was my advisor, and Wiles was his advisor, and my early research was in this area; I have asked several experts in this area of number theory their opinions on the worth of formalising a proof and nobody has shown much interest, in stark contrast to the computer scientists, who view it as some kind of grand challenge).

The appearance of Fermat's Last Theorem on the list is basically a joke I think; the list was written at around the same time that the result was proved by humans.

There are no problems formalising the other two results, it's just that nobody got around to it yet. I would imagine that the Lean community will knock them off within a couple of years (an undergraduate at my university, Kexing Ying, is in the process of formalising martingales, for example). Fermat will be the last one to go, if it ever goes at all.

Answer 2

"Presumably, each theorem presents its own difficulties."

For Fermat's Last Theorem, I agree with the answer by Andrew Wiles' academic grandson and the comments currently on the question. The proof by Wiles was 129 pages long but also very advanced and complicated.

The situation is completely different for the isoperimetric theorem, which has several proofs that can fit on a single-page (see for example this PDF which presents several proofs, some of them being barely more than a page long despite having a lot of space taken up due to the way the integrals were typeset) which don't require nearly as much advanced mathematics (the earliest known complete proof being written in the 1800s). I can't imagine there being any profound obstacles in the formalization of at least one of the many proofs for this theorem, but as already mentioned in Kevin's answer: people have other, more interesting, things to do. Most, if not all, people with enough knowledge to formalize a proof of this theorem, can publish more profound papers if their efforts were dedicated accordingly.

For the optimal stopping theorem (also known as Doob's optimal sampling theorem), the proof is also fairly short, as you can see it fits on this Wikipedia page, but since this theorem is about martingales, presumably we would have to wait until Kevin Buzzard's undergrad student (or someone else) finishes formalizing martingales, before formalizing the entire proof of the theorem.