We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)
It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
> healthy profit margin (as near as we can tell from the outside)
Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.
Whether on net they turn a profit as company overall is neither here nor there.. My point is that they are selling API tokens at a profit (or if being pedantic, then at a price higher than the cost to serve them ignoring research costs). And that that price is got a healthy margin which they don't charge themselves.
Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.
>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.
For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side.
Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?
> 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.
And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.
It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.
While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is a expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.
Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
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?
Back 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].
We'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.
It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.
Most people want more life. For most people it's also the most terrifying part of "the natural human experience".
If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die.
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.
I dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.
I'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.
I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?
First 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. For that I started a project https://github.com/htzh/flt_for_human and contributions are very welcome.
There'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.
> I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. 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).
> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.
> We shared the resulting proof with Kevin Buzzard, who said:
> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
The 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?
This stuck out to me, too. That a (presumably rather simple) coworking tool was instrumental in shaping the vast (6B token!) output is eye-opening. We have this vast power but without intermediate structure it is wasted. Much like Turing machines themselves, which are shaped by language design to get somewhere at the expense of getting everywhere.
I 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.
It 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.
You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead.
my messages are so gloomy because i am heartbroken, that given a technological miracle again, we could snatch tragedy from the jaws of our emancipation.
will you not see that people could be truly empowered and yet will instead be oppressed?
Please tell me how AI is going to make regular people's lives better. You optimisitic types keep saying "just wait, its going to cure diseases" without any outlook on how thats going to happen. You're actually just repeating marketing jargon from AI companies who want people to think they're going to possibly live longer if you let them build more datacenters, so they can make another 30%. Its all about money, thats it.
It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .
And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.
There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.
So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.
True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.
This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.
But how do you know you told it what you intended to tell it?
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.
Note to other users: don’t downvote this kind of comment, answer it.
Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.
Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.
Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.
But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
Holy 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.
Very 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!
It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.
An 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!
The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.
Interesting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen
-and-paper proof feel to them.
Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.
I 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.
Thanks! I've added that link to the toptext.
I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.
I’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.
We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)
"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…"
Gives you an idea of the scale...
It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
> healthy profit margin (as near as we can tell from the outside)
Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.
I don't think Anthropic is turning a profit ;)
Whether on net they turn a profit as company overall is neither here nor there.. My point is that they are selling API tokens at a profit (or if being pedantic, then at a price higher than the cost to serve them ignoring research costs). And that that price is got a healthy margin which they don't charge themselves.
Because of the ongoing training costs. They are certainly making a healthy profit margin on inference.
Neither did Amazon for it's first 25 years ;)
I think you're missing the point of the comment you responded to, lol.
Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.
>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.
Forgive the authors of the article for assuming readers would complete it.
For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side.
Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?
Nah they should have released it in a 14-part tweet instead.
> 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.
And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.
It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Now they have it in writing.
But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.
~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen
It's 6B output tokens, as stated by the blog post.
When writing software with Codex 95+% of tokens are cache, I would assume the same in your case (if you also used it for coding).
What would it cost to make a team of mathematicians do the same?
More importantly how many years it would take.
> 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.
There is no way Fermat could have fit that in the margin. Definitely vindicated.
While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is a expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.
Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
especially compared to existing 129 pages proof by human
Insert meme with 200 pages needed to prove 1+1=2 rigurously
On a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)
one of the most popular books in india growing up. used to see it everywhere
100% It is a very insightful book
i read it from a library. this all just makes me feel cozy and nostalgic and uplifted and sad all at once
Anyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.
This 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
physics is like sex: sure, it may give some practical results, but that's not why we do it
13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)
The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.
> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
They found several bugs and they have patched them. Lots of work going into making sure lean is sound.
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.
Nope! :(
Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!
The proof system is relatively easy to verify.
I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.
You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.
Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
You need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment.
And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.
the Nanoda type-checker for Lean is ~5,000 lines of Rust:
https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...
...and for those who are looking to roll-their-own:
https://ammkrn.github.io/type_checking_in_lean4/title_page.h...
...and some thoughts on putting stuff in the kernel:
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
> 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?
Back 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].
[1] https://arxiv.org/abs/2608.25220
[2] https://github.com/henryrobbins/open-atp
We'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.
It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.
I hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital
Thinking that aging is a natural part of the human experience is a horrible thought? Please explain...
Most people want more life. For most people it's also the most terrifying part of "the natural human experience".
If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die.
There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.
I dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.
Even in a world where these models are heavily restricted, surely the likes of cancer researchers will be among those who have access
I'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.
I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?
Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/
The last box, per https://news.ycombinator.com/item?id=49568667
They released the code here: https://github.com/anthropics/fermats-last-theorem
Looking forward to the 5 billion LoC proof of the Riemann hypothesis.
First 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. For that I started a project https://github.com/htzh/flt_for_human and contributions are very welcome.
More (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.
There'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.
Impressive! Buzzard's group[1] got scooped.
[1] https://github.com/ImperialCollegeLondon/FLT
> What this work is, and is not
> I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. 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).
> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
Seems to have taken it in good spirit:
> We shared the resulting proof with Kevin Buzzard, who said:
> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
The 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?
This stuck out to me, too. That a (presumably rather simple) coworking tool was instrumental in shaping the vast (6B token!) output is eye-opening. We have this vast power but without intermediate structure it is wasted. Much like Turing machines themselves, which are shaped by language design to get somewhere at the expense of getting everywhere.
I 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.
And the multiple Numberphile appearances of Ken Ribet are interesting too! He is incredibly well spoken.
- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)
- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)
Also recommend his other books!
Big Bang - history of the understanding of space and the universe
Code book - history of the maths of ciphers
Haven’t read them for years but I’ve been meaning to again
Ooh I never realized FLT and Code book were the same author. Yes, both great!
It 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.
You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead.
Not sure why anyone is excited about this tech.
So much doom and gloom on this site. Makes it almost not worth reading.
my messages are so gloomy because i am heartbroken, that given a technological miracle again, we could snatch tragedy from the jaws of our emancipation.
will you not see that people could be truly empowered and yet will instead be oppressed?
maybe that's because the doom and gloom is the transparently correct outcome?
Right let's give those AI companies a break, it's not like swarms of autonomous agents are committing felonies
Please tell me how AI is going to make regular people's lives better. You optimisitic types keep saying "just wait, its going to cure diseases" without any outlook on how thats going to happen. You're actually just repeating marketing jargon from AI companies who want people to think they're going to possibly live longer if you let them build more datacenters, so they can make another 30%. Its all about money, thats it.
It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .
And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.
some say it will cure diseases. some, like you, say it will be "100% strictly negative".
i don't really understand either take. nothing else in the world is so perfectly black or white. there will be good, there will be bad.
Well, time to set down the glass beads and dive into a an alpine lake.
I'm so curious what happens to this project that intended on proving FLT by 2029 now
the project: https://imperialcollegelondon.github.io/FLT/
their reaction here : https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
Can 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?
There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.
So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago:
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.
This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.
But how do you know you told it what you intended to tell it?
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.
Note to other users: don’t downvote this kind of comment, answer it.
Isn’t there some theorem that any sufficiently complex mathematical languages will have statements that can’t be proven? :)
This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives.
False negative = could not find a proof of a true theorem.
False positive = erroneous proof of a theorem.
Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.
Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.
No. No human checked it. But a type checker did. And that is much better.
but i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?
Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.
LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?
About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture
That’s just a counter example I can check by hand with almost zero background.
Wiles’s proof will remain a mystery to me.
Come on, you can't compare that with Wiles's proof.
Still unsolved for 87 years.
Lean continues to pay off. Such a beautiful project
An AI safety company!
Why didn't you ran them to find simpler proof? This could also be big.
That's next week's work.
To 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
Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).
Now /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?
Yes. FLT follows from the fact that you can't build the equivalent representation of n-simplex turning into a hypercube in dimensions higher than 2
/s
I call bullshit on 13 million lines makes no sense
Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?
Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.
But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
> Now we add an LLM to that list.
No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...
Holy 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.
that's crazy
Very 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!
https://github.com/anthropics/fermats-last-theorem/blob/main...
13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack.Fable, please translate to HOL-light. Make no mistakes. You are doing great!
It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.
We have a significant case split here:
A human mathematician writes a Lean proof:
- Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases.
An AI writes a Lean proof:
- AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.
I won't be impressed until it identifies the proof he wrote in the margin. /s
An 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!
The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.
If you're doing it for fun anyway, why not use the language that gives you the most pleasure?
Interesting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.
Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.
That's like saying the future of code is Assembler.
Lean is not for humans.
Lean is for humans.
Proving 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.
Formalizing is not the same as discovering. There is still plenty of room for human ingenuity.
> It is truly saddening to think that machines will deprive us of this wonder and experience.
It won't deprive us.
Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art:
https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J
If the Riemann hypothesis is solved primarily by a AI system it will not be as awe inspiring as if a human solved it.
That is just how it is.
Makes me wonder, if we make a tradeoff for comfort and advancement from our biology's "limits" - and that tradeoff is spiritual fulfillment.
Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more
So, 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?
Just loop through all values of a, b, c, and n?
Sure, go on and try it ;)
I found a brilliant proof but there was not enough hard disk space to save the file :(
Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.
If they’re asking that kind of question, do you think this answer will help them understand anything?
maybe it will be an answer that entices them to understand more :)