Nördnytt! 🤓Formalizing Fermat's Last Theorem
- lalitmaganti - 39570 sekunder sedanI suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
Provides great context on this accomplishment, what it means but also doesn't mean.
- sigmar - 39081 sekunder sedan>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
- herbcso - 8649 sekunder sedanSo I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That just feels like a LOT of code to be comletely error-free... What am I missing here?
- glimshe - 29674 sekunder sedan"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order p>=17. This means that their FLT proof only works for p>=17, however FLT was already formalized for odd regular primes by Best-Birkbeck-Brasca-Rodriguez, and the smallest irregular prime is 37, so it’s all good."
My question to any mathematician reading this: does the above make ANY sense to you?
I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.
- cyode - 12915 sekunder sedanI saw the 1996 FLT documentary in high school calculus class. For me, it forever cemented that archetype of modern math researcher at the top of my mental “smart” totem pole.
It also convinced me I had no interest in that path. Setting aside the grinding work of producing a proof that can only be reached by existing years in the abstract and hyper niche isolation of the problem space (not to mention that you might never discover it or that it DNE), the anguish of the output being a paper or presentation or some other artifact of human symbology (_words_, really) that could at any moment be refuted by a single observation of a single mistake—-that sounded like hell to me.
An equivalent high schooler today probably sees things differently, in light of this news and the undeniable implications of LLMs on mathematics. Sturdy autoformalization tooling should with time completely dispel the aforementioned anguish, once our confidence in converting a human proof to Lean/etc. reaches that of a compiler translating Java application language to bytecode. Errata may always exist, but in practice these new methods will do wonders for rigor and peace of mind.
(I’m far less confident re novel discoveries. There’s too much chance of derivative findings based on something part of the training looking like genius but really just tiptoeing on the shoulders of humans, whereas autoformalization is absolutely convincing to me as transformative, particularly to check correctness of AI outputted proofs as mentioned in the post.)
- m_w_ - 39289 sekunder sedan> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
- davmre - 36726 sekunder sedan> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.
At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
- somberi - 38591 sekunder sedanOn a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)
- KaiserPister - 37837 sekunder sedan13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
- Vakaiser - 39235 sekunder sedanWe'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research.
I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging.
The future is both beautiful and terrifying.
- henryrobbins00 - 35263 sekunder sedanBack in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!
I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
- chvid - 36010 sekunder sedanLooking forward to the 5 billion LoC proof of the Riemann hypothesis.
- andrewla - 39518 sekunder sedanWow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/
- mikmoila - 30081 sekunder sedan"The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University."
So in the end, it required tooling crafted by humans.
- aaraujo002 - 39165 sekunder sedanThey released the code here: https://github.com/anthropics/fermats-last-theorem
- sva_ - 17736 sekunder sedanHmm kind of funny, some years ago someone claimed LLMs can do math, and I replied if it could prove fermants theorem:
https://news.ycombinator.com/item?id=33176996#33177939
> Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
> > Shifting the goal posts a bit, aren't we?
I guess the goalposts did change a bit, and in a pretty short time.
- margorczynski - 24941 sekunder sedanWith how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.
- Goofy_Coyote - 5274 sekunder sedanFor math illiterate people like me, my understanding is that FLT was already proven, but the proof was beyond complex, certainly for mere mortals like me, and now Claude has codified it, correct?
- crawshaw - 33529 sekunder sedanMore (strong) evidence that agents make formal methods far more useful. The cost of creating that Lean proof has dropped dramatically.
Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.
- ojo-rojo - 35916 sekunder sedanI'm really impressed by mathematicians. It's cool that Fermat had the intuition to conjecture that "aⁿ + bⁿ = cⁿ" could not be satisfied for n > 2, and that other mathematicians can create proofs, and that others still can understand AI's formulation of those proofs. Really cool.
- kdavis - 39617 sekunder sedanImpressive! Buzzard's group[1] got scooped.
- kristjansson - 39388 sekunder sedanWell, time to set down the glass beads and dive into a an alpine lake.
- throwaboat - 15357 sekunder sedanI wrote a similar DAG-based verifier as a skill a few months ago: https://github.com/sethlei/Warrant . The thing mine has that I didn't see in their's is a verification of the composition rules.
Mine also does more than just math.
- throw567643u8 - 16773 sekunder sedan13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.
LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.
- chi_features - 34998 sekunder sedanThere's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 – highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.
- kzrdude - 37821 sekunder sedanThe part about prove2.me was interesting. That means that a co-working tool was instrumental in the project, and I think AI companies will take note of this. Is this proof specific or will we need to give agents access to JIRA or similar tools to solve large projects in the future?
- vatsachak - 32572 sekunder sedanThis is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it.
If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result
- - 23682 sekunder sedan
- fspeech - 35171 sekunder sedanFirst I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.
- prometheus1992 - 37369 sekunder sedanCan someone with more knowledge help me with this silly question in my head?
>>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems
Did a human check the 13 million lines of code? How does QA'ing this type of work works?
- atleastoptimal - 38906 sekunder sedanIt seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.
- vagab0nd - 32407 sekunder sedan> it wrote 13 million lines of Lean
Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?
- estetlinus - 37874 sekunder sedanI can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
- MichaelDairy - 10055 sekunder sedanI think Anthropic might the frontier lab hiring contractors through data vendors to formalize mathematical textbooks for them at a rate of 170-200 dollars per hour. This was mainly through Alignerr which has the worst reputation for not paying their contractors. They have been hiring since February as far as I can recall. This is in addition to all the internal people they might have working on this. If they have been formalizing all this work for the past 9 months before having Claude use all this data needed to formalize FLT, then it wouldn't be Claude formalizing FLT in just 11 days. Same with the upcoming results they will claim Claude came up with, but in fact they have been hiring frontier researchers working on very niche topics through Micro1. It's all a marketing ploy before their IPO.
- - 36322 sekunder sedan
- black_knight - 30087 sekunder sedanI wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
- - 29074 sekunder sedan
- throw567643u8 - 16123 sekunder sedanI'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.
- dextrous - 18936 sekunder sedanOk, let’s get a rabid pack of agents cranking on P = NP? next!
- vmilner - 26200 sekunder sedanFormalisation of the classification of finite simple groups must be on someone’s ‘moonshot’ list.
- richard_chase - 32184 sekunder sedanAnyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.
- forkbomb123 - 36929 sekunder sedanI'm so curious what happens to this project that intended on proving FLT by 2029 now
the project: https://imperialcollegelondon.github.io/FLT/
- max979 - 22998 sekunder sedanPretty wild seeing this get formalized. Remember struggling to even grasp the high-level concepts of Wiles's proof.
- maw - 28838 sekunder sedanI have discovered a truly marvellous proof of this, which this margin is too narrow bear the load.
- dgellow - 36887 sekunder sedanLean continues to pay off. Such a beautiful project
- enriquto - 34826 sekunder sedanbut i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?
- drivebyhooting - 38005 sekunder sedanLLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?
- jjtheblunt - 30683 sekunder sedan>. Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems.
https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life
It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.
- mnewme - 30680 sekunder sedanDo I miss something? But isnt there the whole code and paper of Kevin Buzzard in the training data of Claude?
- dist-epoch - 22399 sekunder sedanLean required 300 GB of RAM, 96 cores, and took hours to compile and check the formalization.
Now they have the perfect stress test to hill-climb and optimize.
- EGreg - 30535 sekunder sedanSo Fermat’s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?
- - 24571 sekunder sedan
- catigula - 34849 sekunder sedanAn AI safety company!
- ReptileMan - 35917 sekunder sedanWhy didn't you ran them to find simpler proof? This could also be big.
- ex-aws-dude - 37360 sekunder sedanTo ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true?
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
- stabbles - 37522 sekunder sedanNow /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?
- jrflo - 38929 sekunder sedanHoly shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?
- logicallee - 25970 sekunder sedanamazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?
- bluecalm - 38363 sekunder sedanVery impressive! I was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it".
I hope soon enough we will have one of the big ones proved by AI!
- lseplot - 39218 sekunder sedanhttps://github.com/anthropics/fermats-last-theorem/blob/main...
13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack.status: "self-assessed"Fable, please translate to HOL-light. Make no mistakes. You are doing great!
- mhmdfromkarak - 36601 sekunder sedanthat's crazy
- QuesnayJr - 33476 sekunder sedanHoly shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work.
An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.
- victor22 - 33315 sekunder sedanI call bullshit on 13 million lines makes no sense
- threethirtytwo - 30424 sekunder sedan>The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).
What is even the point? Have claude do it.
I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over?
I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.
- saadyousfi - 31127 sekunder sedan[flagged]
- OhNoNotAgain_99 - 30165 sekunder sedan[dead]
- baggy_trough - 39038 sekunder sedanI won't be impressed until it identifies the proof he wrote in the margin. /s
- dakolli - 38363 sekunder sedan[flagged]
- baq - 39270 sekunder sedan[flagged]
- rao-v - 39302 sekunder sedanAn aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable.
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
- refibrillator - 37673 sekunder sedanProving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye:
https://news.ycombinator.com/item?id=49203626
It is truly saddening to think that machines will deprive us of this wonder and experience.
But truly exciting to dream about what lies beyond the limits of our biology.
- anony-123 - 38298 sekunder sedanSo, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ
Can not we do it by code?