11 ms·
Project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover
- racl101 1y agoThese days Fermat would say: "I have an elegant proof but I don't wanna learn LaTex just to publish it."
- generationP 1y agoAnd soon it will be "but I don't want to learn Lean".
- rck 1y agoThis 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 1y 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 1y agoThat 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/ https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".
- golol 1y agoHey Mr. Buzzard I want to say I find your work and enthusiasm with Lean and formalization very cool.
- eig 1y agoSlightly 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: https://imperialcollegelondon.github.io/FLT/ https://imperialcollegelondon.github.io/FLT/
- deleted 1y ago[deleted]
- aardvark179 1y agoThank you. I saw the headline and was thinking things had progress surprisingly quickly.
- ljlolel 1y agoThat’s the title I saw!
- tomhow 1y agoWe've updated the title and URL now, thanks!
- timmg 1y agoSo: 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?
- wk_end 1y agoIt'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.
- School-Cotton 1y agoThe 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).
- Someone 1y agoUnlikely, but not unheard of. Fermat's theorem on sums of two squares is from 1640. https://en.wikipedia.org/wiki/Fermat%27s_theorem_on_sums_of_two_squares https://en.wikipedia.org/wiki/Fermat%27s_theorem_on_sums_of_... says: “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-actually-exists/answer/Senia-Sheydvasser 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)
- prerok 1y agoWell, true, we cannot be 100% certain, but if he published the proof to n=4, we can say it's most likely he did not find the general proof.
- iconjack 1y agoFrom the introduction: "At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof."
- esafak 1y agoWould writing a Lean proof enable algorithmically searching for a shorter (simpler) proof?
- agentcoops 1y agoI worked a long time ago on tools for algorithmically pruning proofs in another theorem-proving environment, Isabelle. That project was largely just using pretty straightforward graph algorithms, but I’m sure the state-of-the-art is much more advanced today (not least it’s an area where I assume LLMs would be helpful conjoined with formal methods).
- lgas 1y agoI'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide: theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := fun hpq : p ∧ q => have hp : p := And.left hpq have hq : q := And.right hpq show q ∧ p from And.intro hq hp To this: theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by exact fun a ↦ id (And.symm a) Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.
- frakt0x90 1y agoI know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once? 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.
- agentcoops 1y agoMore or less! Just like when writing a typical program or indeed mathematical proof, you have a lot of freedom in how you break up the problem into subproblems or theorems (and rely on “libraries” as results already proven). Traditionally the problem with these theorem-proving environments was that the bulk of even relatively basic theorems, let alone the state-of-the-art, had yet to be formalized, so you weren’t quite starting from the axioms of set theory every time but close enough. Lean has finally seen enough traction that formalizing highly non-trivial results starts to be possible.
- sestep 1y agoIf I understand correctly, the only parts you'd need to verify are the core of the theorem prover, called the "kernel" (which is intentionally kept very small), and possibly the code in charge of translating the theorem statement into the language of that core (or you could look directly at the translated theorem statement, which for FLT I'd imagine may be smaller than the code to translate it). Those pieces are orders of magnitude smaller than the proof itself.
- codebje 1y agoYou're basically right, with one teensy caveat: you can't prove the kernel is correct. No model can prove that it is itself consistent, and if you use a more powerful model to prove consistency you're just shifting the goalposts - an inconsistent powerful model can show any model to be consistent. 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!)
- thdhhghgbhy 1y agoA big concern is how future proof this Lean code is, and they are going to produce a lot of it.
- lgas 1y agoI am assuming you mean it's a bigger concern in Lean than other languages because of what people are attempting to do with it (formalize all of math)? Because the language itself, somewhat by design and somewhat by nature, seems to be more future proof than any other language I've ever used.
- thdhhghgbhy 1y agoSo if this project was completed in Lean 3, for sake of example, how compatible would it be with Lean 4 today?
- majikaja 1y agoI think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it. 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.
- joachimma 1y agoTerrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean. https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/ https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t...
- majikaja 1y agoThis is cool I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.
- griffzhowl 1y agoHave you tried "Mathematics in Lean"? It's in the Books section here, along with a few other resources: https://leanprover-community.github.io/learn.html https://leanprover-community.github.io/learn.html
- majikaja 1y agoYes I am aware of this one, it seems like a good intro. 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.
- monkeyelite 1y agoI still don’t understand the excitement here other than it’s related to computers. Will formalizing it make it easier for us to understand the core ideas or arguments? I don’t think it will - that would best be done by reading Wile’s paper which is written with that goal in mind. Given that it was a research frontier where arguments assume an educated audience, it's probably very difficult to formalize.
- kobebrookskC3 1y agothe proof is so complicated it's hard to trust if it's only on paper. if we formalize it, it can be checked by a computer.
- monkeyelite 1y agoy/n of strict logical checking the least interesting part of a proof. It's the insight into why it's true or false that's valuable, and that insight of Wiles was enough to convince the rest of the math community. 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%.
- jibal 1y agoWiles' original proof was flawed. It wasn't due to "sloppy logic", it was a subtle misapplication of a theorem when the conditions for its use weren't met. It wasn't merely a mistake or gap in the exposition ... the error required finding a different approach and it took Wiles and Taylor a year to patch the proof. There are multiple reasons for formalizing the proof in Lean ... see https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md 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.
- gtsnexp 1y agoQuestion for the organizers: Is there an inactivity timeout on claimed sub-problems? Say someone “claims” a task and then goes quiet, others hold back; but without claims, you risk duplicate effort, right? How do you balance that? If there’s a policy already, what counts as “active”? A short status note, a link to a draft, or partial results? If not, would you consider a lightweight scheme: 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.
- deleted 1y ago[deleted]
- jesuslop 1y agoSection #7 is on the Langlands Conjectures. "Conjetures in a proof blueprint?" Curious about the role in the proof. "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 https://tinyurl.com/yc6kth2m)" New math is emerging "as we speak" from the group of Gaitsgory (https://tinyurl.com/9r5bsufj 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.