24
$\begingroup$

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.

$\endgroup$
4
  • 11
    $\begingroup$ Surely FLT doesn't need much of an explanation - the informal proof, counting all prerequisites, is simply very, very long. $\endgroup$
    – Will Sawin
    Feb 8, 2022 at 23:32
  • 2
    $\begingroup$ Some communities are already working towards them. There is a project for FLT on regular primes going on in Lean 3, for example. $\endgroup$
    – Trebor
    Feb 9, 2022 at 6:07
  • 4
    $\begingroup$ @Trebor the regular case is far, far simpler than FLT generally, and we're under no illusions of getting the main result anytime soon :) [I am one of the contributors to flt-regular] $\endgroup$ Feb 9, 2022 at 19:28
  • 2
    $\begingroup$ FLT is in a class of its own (among the 100 theorems) but as far as the other two theorems you mention, it's not clear to me there's much to explain--some theorems had to be the last to get formalized, after all. $\endgroup$ Feb 9, 2022 at 23:58

2 Answers 2

28
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

"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.

$\endgroup$
5
  • $\begingroup$ I wouldn't suggest that the isoperimetric inequality is uninteresting! I would even consider it among the most interesting problems on that list -- in my field of mathematics, it is often cited as the motivation for a new piece of research. Rather, I think it hasn't been formalized because it is more serious a task than you are suggesting. The short proofs in the article you link are all specific to two dimensions. $\endgroup$
    – macbeth
    Feb 9, 2022 at 23:55
  • $\begingroup$ @macbeth I never said it's uninteresting! That's a good point about the link giving proofs for 2D, but more general proofs aren't too long either. A good masters student can formalize a general proof for the isoperimetric inequality :) $\endgroup$ Feb 10, 2022 at 0:03
  • 2
    $\begingroup$ @NikeDattani I don't believe you. If a good masters student can formalise a proof of the general isoperimetric inequality then it would not be still an unsolved problem on Freek's list. Formalisation is hard. A few years ago I made the same mistake: I observed that insolvability of the quintic had not been formalised so I just gave a bunch of undergraduates my notes on the proof and said "just go and formalise this, it's easy". A year later they had got as far as field theory, invented is_scalar_tower, and a year after that a PhD student published a research paper on their invention. $\endgroup$ Feb 13, 2022 at 22:32
  • $\begingroup$ @KevinBuzzard I was worried that someone would say something like that. I intended to be specific that I meant a 2-year research-based master's degree like the ones we have in Canada, rather than the master's degree at Oxford which involves far less than a full year of research. I think I settled on that sentence based on the fact that "good" master's student is subjective enough that the sentence I wrote can be true without making it too long. A good student who has finished their first degree (usually they would have research experience), after another 2 years of full-time work, can do it. $\endgroup$ Feb 13, 2022 at 23:51
  • $\begingroup$ @macbeth I (somewhat belatedly) comment that, based on the prover and proof year given here web.archive.org/web/20080105074243/http://personal.stevens.edu/… it seems that the isoperimetric inequality in the plane, rather than $\mathbb R^n$, is what is meant by "isoperimetric theorem" on the 100 greatest questions list. $\endgroup$
    – Will Sawin
    Jun 28, 2022 at 23:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.