Project to Formalise a Proof of Fermat’s Last Theorem in the Lean Theorem Prover
Key topics
A project aims to formalize a proof of Fermat's Last Theorem in the Lean theorem prover, sparking discussion on the project's scope, the role of formal verification in mathematics, and the potential for discovering new proofs.
Snapshot generated from the HN discussion
Discussion Activity
Very active discussionFirst comment
51m
Peak period
69
0-12h
Avg / period
11.9
Based on 107 loaded comments
Key moments
- 01Story posted
Aug 20, 2025 at 2:27 PM EDT
5 months ago
Step 01 - 02First comment
Aug 20, 2025 at 3:18 PM EDT
51m after posting
Step 02 - 03Peak activity
69 comments in 0-12h
Hottest window of the conversation
Step 03 - 04Latest activity
Aug 25, 2025 at 9:48 PM EDT
4 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
So the title of the paper is misleading at this time.
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?
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).
Suppose Fermat solved the proof by using this natural fault line -its just how this cookie crumbles- solved the n=4 case, and then smashed his head a thousand times against the problem and finally found the prime n proof.
He challenges the community, and since they don't take up the challenge, "encourages" them in a manner that may be described as trollish, by showing how to do the n=4 case. (knowing full well the prime power case proof looks totally different)
1. In any case you view it, it's not trivial, which was the statement in the note. If it were, the effort to publish just for n=4 would be silly, because it would take equal effort to just publish for general case. That he withheld the proof just to mess with people is highly unlikely.
2. I definitely do not make private notes in my books just so that maybe somebody later on would pick up that book and wonder whether I had indeed discovered the secrets of the universe. I definitely do not write "challenges to the community" there.
“Fermat usually did not write down proofs of his claims, and he did not provide a proof of this statement. The first proof was found by Euler after much effort and is based on infinite descent. He announced it in two letters to Goldbach, on May 6, 1747 and on April 12, 1749; he published the detailed proof in two articles (between 1752 and 1755)
[…]
Zagier presented a non-constructive one-sentence proof in 1990“
(https://www.quora.com/What-s-the-closest-thing-to-magic-that... shows that proof was a bit dense, but experts in the field will be able to fill in the details in that proof)
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).
I make notes all the time that I accidentally discover years later with some amusement.
[1]: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Prizes...
This was not obvious at the time, and in fact, Ernst Kummer had discovered the assumption to be false some years before (unbeknownst to Lamé) and laid down foundations of algebraic number theory to investigate the issue.
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 :)
Is Wiles' proof even in ZFC?
Fermat lived before the synthesis of calculus. People often talk about the period between the initial synthesis of calculus (around the time Fermat died) and the arrival of epsilon-delta proofs (around 200 years later) as being a kind of rigor gap in calculus.
But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis. And you occasionally hear other stories that can often be attributed to older mathematicians using a different definition of limit or integral etc than we typically use.
There were some periods and schools where rigor was taken more seriously than others, but the 1600s definitely do not predate the existence of mathematical rigor.
>But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis.
This doesn’t mean that these infinitesimal methods were used in a rigorous way.
One could argue, being a lawyer put Fermat in the more rigorous bracket of contemporary mathematicians at least.
I possess a very simple proof of FLT, and indeed it does not fit in a margin.
I don't ask you to believe me, I just ask you to be patient.
"Don't confuse majority for consensus, soon the majority will flip, but the consensus will stay the same: that there is no consensus."
It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.
The kernels are kept small so that we can reasonably convince ourselves that they're consistent.
The expression of FLT in Lean isn't complicated, because FLT isn't complicated; the kernel language of Lean isn't all that far from the surface language; and the expression "∀ a b c n : ℕ, n ≥ 3 → a ≠ 0 → b ≠ 0 → c ≠ 0 → a^n + b^n ≠ c^n" only needs the infix operators converted to lambda applications (though "only" does a lot of lifting here!)
You can also think of this in reverse and it might help you understand better: Your type checker at compile time is basically providing a sort of "proof" that all the functions and arguments in your program are consistent. Of course, because the type system is not as sophisticated, it can't prove your program is correct, but it as least can prove something about how your program will behave. If you had a more advanced type system, you could, in fact, prove more sophisticated things about the performance of your code (for example that the shapes of all your matrices matched).
A great book on this topic is Type Theory and Formal Proof [1].
0. https://lean-lang.org/functional_programming_in_lean/
1. https://www.cambridge.org/core/books/type-theory-and-formal-...
Advanced proofs essentially just consist of a series of assertions “X, therefore Y, therefore Z, …” and the justification for that isn’t always laid out explicitly. As a result, when you read a formal proof, it often takes some work to “convince yourself” the proof is valid. And if a proof has a mistake, it’s probably not is one of those assertions, but rather in how you get from assertion X to assertion Y. It can often be really subtle.
Disclaimer: I have a math undergraduate, and have played around with the theorem proving language Coq, but haven’t worked with Lean
In the past when proofs were done by hands, little mistakes or little changes could lead to a complete failure of the proof. Mathematicians spent weeks or months to redo the steps and recheck every little detail.
Machine assisted prover basically raises the abstraction level for theorem proving. People don’t need sweat about little details and little changes in the proof steps.
Language based machine provers also enable wider corroboration as a problem can be subdivided into smaller problems and farmed out to different people to tackle, perhaps to different experts for different parts of the problem. Since everyone uses the same language, the machine can verify each part and the overall proof once the parts come together.
https://adam.math.hhu.de/#/g/leanprover-community/nng4
2: The purpose of this is largely for the “writing it” part, not to make checking it easier. The computer checks the validity of the proof. (Though a person of course has to check that the formal statement of the result shown, is the statement people wanted to show.)
I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.
Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.
If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.
https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t...
I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.
https://leanprover-community.github.io/learn.html
I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?
If everything is digitalized no one will have mark homework ever again.
Given that it was a research frontier where arguments assume an educated audience, it's probably very difficult to formalize.
In other words, the chance that we find gaps and mistakes in the written proof? 100% - the chance we find out it's false due to sloppy logic? 0%.
There are multiple reasons for formalizing the proof in Lean ... see https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
P.S. "So that patching is exactly what I’m referring to."
No, it isn't.
"The mathematicians can see the idea that’s true"
Mathematicians could not "see" that FLT was true, and they could not "see" that Wiles' original proof demonstrated it because it didn't. His original flawed proof showed how certain tools could be used, but it didn't establish the truth of FLT. There long had been speculation that it was undecidable, and it might still have been until Wiles and Taylor provided a correct proof.
From a previous comment by the same user: "The purpose of a proof is to show yourself and someone else why something is true."
The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.
The purpose for digitally formalizing a proof of a theorem that has already been accepted as proven by the mathematical community is multifold, as laid out at the link above.
Lean helps with none of that. It doesn’t help you find proof ideas and it doesn’t help you communicate them,
No. The purpose of math is to increase our understanding, not check off boxes.
In your model you might as well have a computer brute force generate logical statements and study those. Why would that be less valuable then an understanding of differential equations?
Some proof assistants contribute more directly to understanding by making proofs easier to study.
In fact, Buzzard has an "existence theorem" of this exact thing. Annals of Mathematics (one of the top mathematics journals) has published one paper proving a theorem, and another paper proving the opposite result of a theorem: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...
The purpose of a proof is to show yourself and someone else why something is true. I don’t know what it would mean to be writing them for computers to verify. Unless the only thing you are interested in is y/n
Human verification can never be ruled out entirely with these sorts of systems: you always have to check that the definitions used in the final statement mean what you think they mean, and that all of the base axioms are acceptable.
And of course, there's always the possibility of bugs in the kernel. I even recently found a bug [0] in a verifier for Metamath, which is designed to be so simple that its only built-in logic is typed string substitution. But such bugs should hopefully be unlikely in non-adversarial settings.
[0] https://github.com/metamath/metamath-exe/issues/184
https://youtu.be/Dp-mQ3HxgDE?si=8a0d6ci-7a-yfhou
"It will not be the original Wiles/Taylor-Wiles proof, but rather a "newer" proof which takes into account more recent developments due to Khare-Wintenberger, Kisin and many other people."
Soft claim (one task per person); progress update within 7–14 days (longer for big items); auto-release if no update; extensions on request; Tag some tasks as “pairable” so two people can collaborate openly.
Curious how you’re handling throughput vs inclusion here.
"The { Wiles } modularity theorem { that cracked FLT } is a special case of more general conjectures due to Robert Langlands. The Langlands program seeks to attach an automorphic form or automorphic representation (a suitable generalization of a modular form) to more general objects of arithmetic algebraic geometry, such as to every elliptic curve over a number field. Most cases of these extended conjectures have not yet been proved. (https://tinyurl.com/yc6kth2m)"
New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj), but apply to the (differential) geometric Langlands area, while the quote looks about the algebraic-geometry area (of Weil's triple Rosetta Stone). Yet areas have well understood connections. Both kind of works (new math and formalizing) are very needed. Verifiable proofs have to help to avoid math building collapsing under own weight/richness.