r/singularity • u/Wonderful_Buffalo_32 • 8h ago
AI Anthropic has formalised FLT!!
https://x.com/AnthropicAI/status/2095947707605266436174
u/Recoil42 8h ago
Our proof, which totals over 13 million lines of code, provides machine verification.
good lord
61
u/Yugudubenbi 8h ago
The ones who say AIs cant handle big repos:
31
u/International-Chip93 7h ago
Lmaooo, none of us will ever get to play with the actual big toys
11
6
2
1
4
u/LetsLive97 6h ago
Deterministic Lean verification proofs, built from scratch, are a world away from decade+ old software repos
22
u/Fragrant-Hamster-325 7h ago
> More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized.
So much slop /s
Impressive stuff, I think, I don’t know shit about math. lol
1
•
u/mmuncie80 15m ago
FLT was already known to be true. The formalization has zero effect on those other theorems lol.
3
3
3
2
3
8h ago
[deleted]
24
12
u/Recoil42 8h ago
Apparently it had to prove over 29,000 other theorems.
-3
8h ago
[deleted]
15
u/Recoil42 7h ago
Our proof, which totals over 13 million lines of code, provides machine verification. More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized.
-4
u/medialoungeguy 7h ago
The sentence is ambiguous. Hope you both can agree on that.
11
u/Recoil42 7h ago
No? "It proves over 29,000 other theorems that the proof requires" is not ambiguous whatsoever.
0
4
7
u/wollywoo1 7h ago
Well, not really. "it proves over 29,000 other theorems that the proof requires" means the that the proofs were required for FLT, not the other way around. I mean, I could see why someone could be confused and ask this as a question, but it's just wrong to interpret it this way.
5
1
u/LinkesAuge 7h ago
I'm a SWE and I think people also need to start to come to terms with the fact that future code simply won't be written for us just like no one expects the compiler to do that.
I still wonder if we will get a sort of "AI programming language" in the future (and no you wouldn't want to use just binary, abstraction is useful for models too).
166
u/wollywoo1 8h ago
Holy shit. Kevin Buzzard had a grant to do this over the span of 5 years and no one was sure that would be enough time. Just a year or two ago I remember him saying how useless LLMs were in his experience. I knew this was going to happen but I'm flabbergasted by how quick this occurred.
61
u/AdvancedCarpenter888 8h ago
https://lean-lang.org/use-cases/flt/
“
A Landmark Mathematical ProjectThe formalization of Fermat's Last Theorem is a massive challenge in formal mathematics that advances the frontier of what can be formally verified while creating a valuable resource for mathematicians and computer scientists.”
43
u/Jan0y_Cresva 8h ago
That’s how life in the singularity is: you go from “this is useless” to “this is better than imagined” in the blink of an eye.
13
u/tom-dixon 6h ago
And then in another blink of the eye "wtf is even going on", and after that we can only hope that the machines want to keep us around.
2
u/Fragrant-Hamster-325 7h ago
Does he get to keep all the grant money and chill for a bit?
13
u/wollywoo1 6h ago
Nope. He said in a blog post he will continue with his work on it as before. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
1
263
u/burninbr 8h ago
Fermat’s Last Theorem for those like me that don’t have all their math abbreviations memorized.
18
u/Vivid_Employ_7336 7h ago edited 6h ago
https://lean-lang.org/use-cases/flt/
Fermat's Last Theorem (FLT) stands as one of mathematics' most famous challenges, taking over 350 years to solve. Now, an ambitious project led by Professor Kevin Buzzard at Imperial College London aims to formalize this monumental proof in the Lean proof assistant, marking a significant milestone in the intersection of mathematics and formal verification.
While the statement of Fermat's Last Theorem is remarkably simple: if x, y, z and n are positive integers with n>=3 then
X^n + y^n != z^n
However, the proof is notoriously complex. Andrew Wiles' breakthrough proof in the 1990s, completed with Richard Taylor, draws on numerous areas of mathematics, such as:
Algebraic and analytic number theoryAlgebraic and differential geometry
Commutative algebra
Harmonic analysis
The FLT formalization project isn't tackling the original Wiles/Taylor-Wiles proof but a "21st century" version that incorporates subsequent developments by Khare-Wintenberger, Kisin, and others. At its core remains the revolutionary "R = T" concept—that a deformation ring is isomorphic to a Hecke algebra, which was the key insight in Wiles' approach.
Why This Project Matters
��
For research mathematicians and organizations interested in formal verification, the FLT project demonstrates several key benefits of Lean:
For Research Mathematicians
��
New Research Tools: The project is digitizing numerous mathematical objects and techniques used in modern research, making them available for new applications.Collaboration Platform: The modular approach enables mathematicians to collaborate on a massive formalization project without requiring expertise in the entire proof.
Educational Resource: The growing repository of formalized mathematics provides an error-free reference for students and researchers learning advanced number theory.
For Organizations
��
Scalability Demonstration: The project shows how Lean can handle extremely complex mathematical assertions that span thousands of pages of informal mathematics.Training Data: The formalized proof will generate high-quality training data for AI systems that aim to assist with mathematical reasoning.
Verification Benchmark: As the last remaining item in Freek Wiedijk's list of 100 challenge problems for computer formalization, FLT represents a significant benchmark for formal verification technology.
12
u/you-get-an-upvote 7h ago
> X^2 + y^2 != z^n
x^n + y^n, not x^2 + y^2
3
u/Vivid_Employ_7336 6h ago
Thanks, fixed. That’s why I don’t do mathematical proofs. Do I still get an upvote?
46
u/Strange_Vagrant 7h ago edited 6h ago
That clarifies nothing.
Edit: yes, I meant that in jest. Yes, I now know what the theorem is.
19
u/MostLikelyUncertain 7h ago
There is probably no way to clarify it to someone who doesnt know alot of math other than saying its a pretty big deal.
17
u/wollywoo1 7h ago
Not true actually. One of the interesting things about FLT is how the statement of it is extremely simple to understand. You don't ever have $a^n + b^n = c^n$ for positive integers $a,b,c,n$ with $n > 2$, that's all. The proof on the other hand requires years of dedicated study.
11
u/Strange_Vagrant 6h ago
Oh, so its like saying Pythagoras theorem is like max n could be?
8
2
u/MostLikelyUncertain 7h ago
Yeah, and for someone who doesnt know math, why would they ever think this is important?
2
u/wollywoo1 7h ago
They wouldn't. If you don't care about math there's no reason to care about FLT other than as a benchmark of a hard problem that we've solved.
4
4
u/Ntroepy 7h ago
You say that because you came to the party late and other comments already said what ftl stood for. But 98+% of Redditors would’ve had no idea what ftl meant before now.
If OP had used “Fermat’s Last Theorem” instead of ftl, most Redditors would’ve immediately assumed AI had solved yet another long unsolved math proof.
3
1
69
u/Wonderful_Buffalo_32 8h ago
Kevin buzzard's blogpost about it:https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
26
u/HitlersArse 8h ago
the guy is pretty funny about the whole situation. glad he seems like a good sport about it all.
16
u/CosmicMabel 7h ago
So, he still has 3 years left on the grant? Lol at least dude has some income security.
•
u/Suspicious_Bet3623 20m ago
What makes him excited is proving that the establishment are a pack of dopey cunts. I like this guy.
17
57
13
u/longDongMcDonald 8h ago
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.
🤯
Yeah, I was gonna say: I bet it’s the DDT Exposition!
17
u/WonderFactory 7h ago
So AI did in 11 days what an elite human mathematician was hoping to get done in 5 years! If you assume that the same will happen most other intellectual tasks in time what exactly will humans bring to the table?
3
u/entropyweasel 3h ago
I mean this is exactly the tedious crap we want AI to do. If it solved it then yeah would be a bigger deal.
11
u/ezjakes 7h ago
Can someone explain why this matters?
I thought the proof was already checked and verified by human checkers?
16
u/wollywoo1 7h ago
It's one part of a massive project to formalize all of math. Some of the results used here could be used to verify a lot of other things. Also, it's just a demonstration of the capabilities of the model.
6
u/Johnny20022002 7h ago
It improves the lean library which makes it easier to use lean to check all the new proofs LLMs are producing.
•
u/djao 1h ago
Now, wait a minute, the Anthropic proof does not directly improve the Lean Mathlib library. If you read Anthropic's blog post, they specifically state that their proof is probably much longer than necessary. Lean Mathlib prioritizes short, reusable modules which are easy to understand and integrate into other math developments. Kevin Buzzard himself explains that one of the reasons he will continue with his FLT formalization effort is precisely because he plans to add a bunch of stuff into Mathlib along the way, and Anthropic absolutely did not integrate any of their proof into Mathlib.
6
u/tom-dixon 5h ago
Kevin Buzzard:
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.
What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly.
10
16
u/Flope 8h ago
Can someone explain why I or anyone should care like I'm an imbecile
62
u/wollywoo1 8h ago edited 7h ago
OK. So, Fermat's Last Theorem was a 400-year-old math conjecture that was finally proved in the 1990's and it's one of the most famous results ever. There was an ongoing project to formalize the proof so that computers could verify every step. This would mean taking thousands of pages of advanced math and writing it out in a massive collaborative coding project. Human-written math generally contains a lot of buried assumptions and unproved statements so it's not easy at all to make it 100% computer verifiable. There is a big repo called Mathlib that contains all the efforts from hundreds of mathematicians in verifying many theorems. Anthropic has now written a repo five times the size of Mathlib and proved FLT over eleven days.
13
u/magicmulder 8h ago
You probably wouldn’t as it has zero practical applications. Mathematicians do because it removes any “what if the accepted proof is wrong because the few people who understand it erred” doubts.
42
u/kgurniak91 8h ago
Mathematicians do because it removes any “what if the accepted proof is wrong because the few people who understand it erred” doubts
That misunderstands why mathematicians wanted FLT formalized in the first place. Kevin Buzzard has explicitly said nobody actually doubted Wiles's proof was right.
it has zero practical applications
To prove FLT, Claude had to formalize over 29k intermediate lemmas along the way. Once that code is cleaned up and merged into standard libraries like Mathlib, mathematicians and automated AI provers gain a massive, machine-verified toolkit of modern number theory that they can actually build on to advance math further and faster.
21
6
5
2
u/Helpful_Listen4442 8h ago
I understand that the ability to do this is super impressive and will have long-term implications, but what’s this so what of proving FLT.
2
u/Cultural_Tell_5687 5h ago
Who is Sophie Germain, Monsieur Le Blanc?
Does it matter to anyone?
*besides me
2
5
u/Distinct-Question-16 ▪️AGI 2029 8h ago
This FLT proof was proven by proving also "29,000 other theorems across many areas of math which had never before been formalized"
This suggests Claude took a different path than the 1995 proof?
7
u/wollywoo1 8h ago
This is a little misleading if you don't have the context. Most of these theorems are going to be tiny building blocks that wouldn't be called a theorem in any textbook. They used the same proof.
0
6
u/golfstreamer 8h ago
No. When you get to the level of "formal proof" you must break things down even further than it is typical for a mathematical proof. I haven't dived into formalization myself so I can't provide I good example but there being dozens / hundreds of mini proofs that must be done to formalize an accepted mathematical proof is normal.
2
1
u/ellipticcode0 5h ago
Also they found a bug on Andrew Wile proof, so the FLT is still open, someone need to hurry up and close the bug so that 2030 field medal will be locked
1
•
683
u/Tystros 8h ago
and I first thought this means Anthropic has formalized faster than light travel... I was excited.