Slightly misleading title- this is the overall blueprint for a large ongoing effort by the Imperial College London to formalize FLT in Lean, not the proof itself (which is huge).
The project webpage has more information about the efforts and how to contribute:
Thank you. I saw the headline and was thinking things had progress surprisingly quickly.
iconjack · 2m ago
From the introduction: "At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof."
timmg · 1h ago
So: as I understand it, Fermet claimed there was an elegant proof. The proof we've found later is very complex.
Is the consensus that he never had the proof (he was wrong or was joking) -- or that it's possible we just never found the one he had?
jerf · 54m ago
There is known to be a number of superficially compelling proofs of the theorem that are incorrect. It has been conjectured that the reason why we don't have Fermat's proof anywhere is that between him writing the margin note and some hypothetical later recording of the supposed proof, he realized his simple proof was incorrect. And of course, saw no reason to "correct the historical record" for a simple margin annotation. This seems especially likely to me in light of the fact he published a proof for the case where n = 4, which means he had time to chew on the matter.
jacquesm · 14m ago
Or, maybe he had a sense of humor, and made his margin annotation knowing full well that this would cause a lot of headscratching. It may well be the first recorded version of nerdsniping.
ljlolel · 5m ago
More likely he decided to leave it in as a nerdsnipe rather than he wrote it in the first place as a nerdsnipe (seems more likely he thought he had it?)
jfengel · 59m ago
Fermat lived for nearly three decades after writing that note about the marvelous proof. It's not as if he never got a chance to write it down. So it sure wasn't his "last theorem" -- later ones include proving the specific case of n=4.
There are many invalid proofs of the theorem, some of whose flaws are not at all obvious. It is practically certain that Fermat had one of those in mind when he scrawled his note. He realized that and abandoned it, never mentioning it again (or correcting the note he scrawled in the margin).
mdiesel · 57m ago
He probably did know it, it's remarkably simple. I can't remember how to format maths in a HN comment though to put it here.
prerok · 2m ago
Yeah, I just figured out how to simply reconcile general relativity and quantum mechanics, but I am writing on my phone and it's too tedius to write here.
wk_end · 1h ago
It's possible we never found the one he had, but it's pretty unlikely given how many brilliant people have beaten their head against this. "Wrong or joking" is much more likely.
Xcelerate · 23m ago
I feel like there’s an interesting follow-up problem which is: what’s the shortest possible proof of FLT in ZFC (or perhaps even a weaker theory like PA or EFA since it’s a Π^0_1 sentence)?
Would love to know whether (in principle obviously) the shortest proof of FLT actually could fit in a notebook margin. Since we have an upper bound, only a finite number of proof candidates to check to find the lower bound :)
umanwizard · 1h ago
The former.
We can't be 100% certain that Fermat didn't have a proof, but it's very unlikely (someone else would almost surely have found it by now).
hokkos · 28m ago
I also have an elegant proof, but it does't quite fit in a HN comment.
ape4 · 1h ago
Its a "dog ate my homework" situation
racl101 · 1h ago
These days Fermat would say: "I have an elegant proof but I don't wanna learn LaTex just to publish it."
rck · 1h ago
This is the Lean blueprint for the project, which is a human-readable "plan" more or less. The actual Lean proof is ongoing, and will probably take a few more years. Still cool though.
cubefox · 1h ago
> At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a
sketch proof. Over the next few years, we will be building parts of the argument, following a
strategy constructed by Taylor, taking into account Buzzard’s comments on what would be
easy or hard to do in Lean.
So the title of the paper is misleading at this time.
kevinbuzzard · 1h ago
That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".
golol · 1h ago
Hey Mr. Buzzard I want to say I find your work and enthusiasm with Lean and formalization very cool.
The project webpage has more information about the efforts and how to contribute:
https://imperialcollegelondon.github.io/FLT/
Is the consensus that he never had the proof (he was wrong or was joking) -- or that it's possible we just never found the one he had?
There are many invalid proofs of the theorem, some of whose flaws are not at all obvious. It is practically certain that Fermat had one of those in mind when he scrawled his note. He realized that and abandoned it, never mentioning it again (or correcting the note he scrawled in the margin).
Would love to know whether (in principle obviously) the shortest proof of FLT actually could fit in a notebook margin. Since we have an upper bound, only a finite number of proof candidates to check to find the lower bound :)
We can't be 100% certain that Fermat didn't have a proof, but it's very unlikely (someone else would almost surely have found it by now).
So the title of the paper is misleading at this time.