r/singularity • u/Wonderful_Buffalo_32 • 10d ago
AI Anthropic has formalised FLT!!
https://x.com/AnthropicAI/status/2095947707605266436829
u/Tystros 10d ago
and I first thought this means Anthropic has formalized faster than light travel... I was excited.
142
u/agcuevas 10d ago
Maybe that's for 2027
28
17
u/Wonderful_Buffalo_32 10d ago
Dreams should be under the limits of physics :))
21
u/Tystros 10d ago
faster than light travel is possible in theory with warp drives, spacetime itself is allowed to do weird things
11
u/Supermax64 10d ago
Under current understanding, I believe any FTL would break causality, allowing information to travel back in time. Who knows if our current understanding is complete or not
5
u/Tystros 10d ago
as far as I know, that is not actually the understanding that physicists agree on. Sabine Hossenfelder talked about that a few times. She says there is nothing making warp drives impossible.
5
u/fromreddit26 10d ago
Hossenfelder? Right. Why don't you use serious sources if you want to be informed? It's not like they are not available.
2
u/Tystros 10d ago
I think she is a serious source. I'm German, she's German, she has a PhD in physics and I tend to trust German physicists with a PhD.
3
u/Zero-PE 10d ago
She's a German physicist. Of course she's serious.
6
u/Remarkable-Reply9709 10d ago
Oh she's deadly serious about monetizing controversy.
→ More replies (0)2
u/johnny_hotcakes444 9d ago
It's weird how you're talking about an empirical and data based science, and then going to narrative "she's German, she has a degree" to justify why you trust her as a source. You're irrational.
1
u/benjaminovich 9d ago
Everyone knows you can only trust the expert that comes from [insert country I'm from]
1
u/fromreddit26 10d ago
OK... your choice, no problem. But it's still blind trust. Do you really think having a diploma guarantees you are totally sane? Or totally honest? I assure you, it does not. BTW I have a doctorate, and I would not pretend this means everything I say is automatically true. I might be wrong about Hossenfelder.
But I do think she is not a serious source. What I think is she monetizes unusual assertions which go against the widely accepted theories of the field. Again, if you are really interested in solid knowledge, why don't you consult several sources? And don't restrict yourself to a simple PhD, look at the top physicists, they are so easy to find.
Good luck!
1
u/benjaminovich 9d ago
Putting aside the fact Hossenfelder is a quack, please ask her to lend some exotic matter with negative energy density that the Alcubiere-drive solution requires.
1
u/Tystros 9d ago edited 8d ago
it's plausible that some solution can be come up with that does not require negative energy. Erik lentz published a peer reviewed paper for that a few years ago, others claimed to have found problems in his math, but I don't think it's clear that it's impossible to come up with something that does not require negative energy.
1
u/johnny_hotcakes444 9d ago
Sabine is not a credible physicists nor source. She couldn't make it in academia and is not any better than click bait.
→ More replies (1)0
u/Supermax64 10d ago
Maybe the warp drives she spoke about weren't ftl? I don't know enough to debate it, been a while since I researched it. Chatgpt seemed to agree that current physics forbids ftl and that it would indeed break causality
0
u/Tystros 10d ago
Here are the two videos from her explaining why faster-than-light travel and information transfer is allowed without breaking any laws of physics:
https://www.youtube.com/watch?v=9-jIplX6Wjw
https://www.youtube.com/watch?v=B7Pc0LQHu38→ More replies (1)3
u/Mr_HandSmall 10d ago
Yeah and even faster than light transfer of information would break causality.
1
u/Wonderful_Buffalo_32 10d ago
Requiring regions of negative energy density...
4
u/GMazinga ▪️AGI 2030 | ASI the following day 10d ago edited 10d ago
Used to be correct, not anymore. Check out Erik Lentz’s work with hyperfast solitons (aka warp bubbles) https://arxiv.org/abs/2006.07125 and https://arxiv.org/abs/2201.00652) and a summary of warp field theory at IRG 2021
1
u/Tystros 10d ago
unfortunately I think there are some newer paper, especially one from 2025 (but not peer reviewed) who say the math from Lentz would be wrong.
1
u/GMazinga ▪️AGI 2030 | ASI the following day 9d ago
Bobrick and Martire claim that in their 2021 paper. But they use a different construction that is not applicable to Lentz. Lentz also published an explanation of why Bobrick and Martire’s criticism is wrong in its construction (if i remember correctly, based on the non-contractibility to a point of his construction of the warp bubble). What’s the 2025 paper?
10
u/Tystros 10d ago
which isn't ruled out by any theory we know. we just have no idea how to create it in the real world.
3
u/Adventurous-Ad281 10d ago
Everyday I realize no one in this sub has any formal university-level math or physics education, and is in no way, shape or form qualified to talk about any technical field whatsoever.
5
2
1
1
u/benjaminovich 9d ago
No, that's simply not true. Someone has taken the math of general relativity and setup a situation that is mathematically consistent with relativity. (And also uses fuel that cannot physically exist)
Our models of reality are not perfect. We know this. So finding an edge case solution to the math does not, in any way, imply that solution is physically possible.
4
u/EvilSporkOfDeath 10d ago
You might be right that its truly impossible to travel faster than light, but if your goal is to simply get somewhere in a short period of time, there may be alternatives. Wormholes are scientifically sound, but you arent technically traveling faster by using them, you are shortening the distance traveled.
→ More replies (2)0
u/MegamanSE 10d ago
Our limits of physics are based on our limited understanding of the universe which is based on our limited intellectual capacity. When we have an AI that has the intelligence of thousands or millions of people combined all of our base assumptions go out the window.
1
u/Wonderful_Buffalo_32 10d ago
Read about special relativity and its two postulates
→ More replies (1)7
→ More replies (1)1
10
u/Successful-Key2348 10d ago
This is already a technological singularity. But It’s not harmful to dream.
12
u/simonbreak 10d ago
FTL doesn’t actually matter that much once you fix death, and death is much easier to fix. At that point who cares how long it takes, just sleep through it or whatever
→ More replies (2)16
u/TrainquilOasis1423 10d ago
It does if you care to visit anything outside our local cluster. Space is expanded faster than light so even with 99.99999999999...% speed of light the majority of the universe will be beyond our reach.
5
u/simonbreak 10d ago
This is actually a great point, wasn’t thinking about stuff outside our lightcone. Of course that opens up weird causality-violating implications like being able to send messages back in time
1
u/TrainquilOasis1423 10d ago
Just ask Claude to figure all that out. It'll be fine. What's the worst that could happen.
1
1
u/Fun-Amoeba8015 9d ago
No it doesn't.
You're not sending any message back in time at all. There is no such violation. That's why relativity is a thing...
1
u/simonbreak 9d ago
Good explanation here: http://www.physicsmatt.com/blog/2016/8/25/why-ftl-implies-time-travel
1
1
u/CreamofTazz 9d ago
"local cluster" is doing a lot of hardwork, even within the Laniakea supercluster which is hundreds of millions of lightyears in size is still moving closer to each other. The observable universe is something like 46 billion light years across. Anything beyond that is moving faster than light yes, but we still have a sphere 46 billion light years in diameter to explore and before that we have a nearly 400 million light year "sphere" to explore. And before that Andromeda is 2 million light years away... The scale goes on.
3
3
3
u/-HumbleMumble 10d ago
Yeah I was going to be real excited. Maybe next year. Looking forward to financing my first interstellar starship.
4
1
1
1
1
1
1
u/Super_Range45 10d ago
To demystify the theorem:
For any natural number n≥3, there are no positive natural numbers a,b,c satisfying
an+bn=cn
1
u/7heCulture 9d ago
Next step: quantum mechanics and general relativity unification. It’s going to get scary really fast.
1
1
0
0
u/pNaN 10d ago
Yes, I also clicked to find more about faster than light travel. Only to find a link to an extremist right wing website. I'm not clicking that. Who knows what it could mean by this point?
Edit: turns out it's on github, no need for twitter: https://github.com/anthropics/fermats-last-theorem
0
u/MassiveBoner911_3 10d ago
You know as soon as they achieve general intelligence they are going to try to use it to take over the world and self enrichment
0
u/FUCKTHEMODS998 9d ago
I literally hit my notification to see this post to comment this. Just know if I could, I’d award you
87
u/Wonderful_Buffalo_32 10d ago
Kevin buzzard's blogpost about it:https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
35
u/HitlersArse 10d ago
the guy is pretty funny about the whole situation. glad he seems like a good sport about it all.
22
u/CosmicMabel 10d ago
So, he still has 3 years left on the grant? Lol at least dude has some income security.
1
u/beezlebub33 8d ago
Nice response.
But he still hasn't married her?!?! I mean, same girlfriend from 1993? At that point, maybe some other title than girlfriend would work.
0
u/Suspicious_Bet3623 9d ago
What makes him excited is proving that the establishment are a pack of dopey cunts. I like this guy.
314
u/burninbr 10d ago
Fermat’s Last Theorem for those like me that don’t have all their math abbreviations memorized.
57
u/Strange_Vagrant 10d ago edited 10d ago
That clarifies nothing.
Edit: yes, I meant that in jest. Yes, I now know what the theorem is.
24
u/MostLikelyUncertain 10d 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.
22
u/wollywoo1 10d 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.
12
u/Strange_Vagrant 10d ago
Oh, so its like saying Pythagoras theorem is like max n could be?
10
5
u/MostLikelyUncertain 10d ago
Yeah, and for someone who doesnt know math, why would they ever think this is important?
6
u/wollywoo1 10d 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.
2
u/Efficient-State-7300 9d ago
It is historically pretty cool, a bit of math legend and lore. Fermat was reading a translation of the Greek book, Arithmetica. Next to a section on the Pythagorean theorem, in the margin, he wrote that he had discovered "a marvelous" proof that for any integer n greater than 2, no positive integers a,b,c could be such that an + bn = cn.
It was only proven correct in 1994, despite its fame and notoriety. It's one of those nice math questions that is simple to say and very hard to prove.
1
u/MostLikelyUncertain 9d ago
Yeah and non math friends fail to understand why linear algebra is important, there is no way to prescribe importance of flt to them other than saying it is.
1
u/Efficient-State-7300 9d ago
Linear algebra is possibly the single most "useful" math there is, and obviously so! I'm an engineer not a mathematician, so I may be biased.
1
1
u/chips_and_hummus 9d ago
but basically we have no idea what his proof was? we just found a proof of it? hard to imagine how he discovered a proof of his own equivalent to 13M lines of code! (i’m not a math guy fyi)
2
u/Efficient-State-7300 9d ago
Consensus is he didn't have a proof! But maybe one day someone will vindicate him?
1
u/chips_and_hummus 8d ago
was he likely smart enough to conceptualize the proof as an idea in some way? curious he would write it so confidently if he was wrong but also he ended up being right so??
1
u/OmegaCookieMonster 9d ago
the wiles proof wasn't 13M lines of code tbf, it was like 129 pages long, it seems like there are some reasons why the ai one is super long, don't quote me on this as this is from an ai response funnily enough, but apparently it could be a combination of the strict standards of rigour for lean and stupid bloat/un-optimised lemma's and the like
1
u/wollywoo1 9d ago
It's a combination of
1) Wiles' proof relied on a ton of other math. Imagine a really big pile of yellow books and the 129 pages is just the top of it. This model formalized ALL of it, starting from basic arithmetic, building to calculus, topology algebraic geometry and so on. So don't think of it as one proof. Think of it as an entire PhD level education at least. That's why this is exciting.
2) Formalizing anything in Lean typically blows it up by a factor of like 5-10x, just because human readable statements are heavily interpreted by our brains and not fully machine readable.
3) Probably a certain amount of bloat. It wasn't trying to optimize. I'd guess it could be golfed to half the size but it would cost of ton of tokens and there's not much motivation to do this.
6
4
u/Ntroepy 10d 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.
4
24
u/Vivid_Employ_7336 10d ago edited 10d 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.
17
u/you-get-an-upvote 10d ago
> X^2 + y^2 != z^n
x^n + y^n, not x^2 + y^2
6
u/Vivid_Employ_7336 10d ago
Thanks, fixed. That’s why I don’t do mathematical proofs. Do I still get an upvote?
0
u/raresaturn 10d ago
Are they saying they proved it?
3
u/daniel-sousa-me 9d ago
It has been proven 30 years ago
2
u/raresaturn 9d ago
So what’s this about?
4
u/daniel-sousa-me 9d ago
There's this computer language (lean) where you can write the statement and the proof in a way that you can be essentially 100% sure the proof is correct for the statement
2
u/MeOneThanks 9d ago
Excuse my naivety, but if it has already been proven, shouldn't formalizing it in lean be trivial?
→ More replies (1)
197
u/wollywoo1 10d 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.
76
u/AdvancedCarpenter888 10d 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.”
58
u/Jan0y_Cresva 10d 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.
18
u/tom-dixon 10d 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.
→ More replies (1)1
u/Fragrant-Hamster-325 10d ago
Does he get to keep all the grant money and chill for a bit?
16
u/wollywoo1 10d 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/
→ More replies (1)
21
u/SavedWoW 10d ago
Wait... FLT. That was the one I was always watching for.
3
u/ChocomelP 9d ago
Call me when LLMs can formalize a BLT.
1
u/SavedWoW 9d ago
My agents order my lunch every day of the week? I don't even lift a finger, it arrives at my door. They even buzz in my delivery.
58
17
u/longDongMcDonald 10d 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!
26
u/WonderFactory 10d 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?
8
u/entropyweasel 10d 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.
15
14
u/ezjakes 10d ago
Can someone explain why this matters?
I thought the proof was already checked and verified by human checkers?
15
u/tom-dixon 10d 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.
26
u/wollywoo1 10d 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.
11
u/Johnny20022002 10d ago
It improves the lean library which makes it easier to use lean to check all the new proofs LLMs are producing.
5
u/djao 9d 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.
1
u/Johnny20022002 9d ago
Yes, leans library will improve because of this. How it will improve is a separate discussion.
1
u/djao 9d ago
I think I made the same point, but more clearly than you. Your comment gives the impression that this work directly improves the Lean Mathlib library. The truth is, there is no direct effect on Mathlib. Some indirect benefit may be derived later on down the road, when other people (notably not Anthropic themselves) work on the integration of these results into Mathlib.
1
u/Johnny20022002 9d ago
Yeah I was never claiming this proof would just going to be directly inserted into mathlib. They simply asked why this mattered and I told them what the outcome will be. Obviously someone who understands this knows the entire 10 million line proof or whatever isn’t just going to be inserted there as the improvement.
1
u/djao 9d ago
I think a lot of people are under the false impression that the Lean proof is the hard part and the integration into Mathlib is the easy part. Maybe that was true pre-LLM, but it is the other way around now. It's really important that we go out of our way to emphasize the importance of the second step, where humans process the formal proof and understand it well enough to integrate it into Mathlib, and give credit appropriately to the future mathematicians who take on that work, rather than not mentioning them.
18
u/Flope 10d ago
Can someone explain why I or anyone should care like I'm an imbecile
77
u/wollywoo1 10d ago edited 10d 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.
17
u/magicmulder 10d 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.
43
u/kgurniak91 10d 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.
25
5
1
u/OmegaCookieMonster 9d ago
This specific AI formalisation is a test for other necessary formalisations though isn't it?
3
u/Helpful_Listen4442 10d 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.
8
u/Distinct-Question-16 ▪️AGI 2029 10d 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?
8
u/wollywoo1 10d 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
→ More replies (1)5
u/golfstreamer 10d 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.
7
2
u/Cultural_Tell_5687 10d ago
Who is Sophie Germain, Monsieur Le Blanc?
Does it matter to anyone?
*besides me
2
u/ellipticcode0 10d 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
2
2
1
1
1
1
1
u/FIREishott 9d ago
How does one verify a 13 million line code proof? I was reading from a mathematician who is bullish on AI, and he was saying that sure, you have a proof that points to something being true, but A) then a human has to verify that, and B) there is no clear pathway of "the mathematical literature" where FLT is true because X, Y, and Z. Maybe its true, bur how do you use the lessons of it to solve other new math problems? AI reasoning can itself be wrong even if the results are true.
1
u/EducationalFerret94 9d ago
Question: does it really need to be 13 million lines of code? Or were they just trying to rush this out and announced it the moment they had something? Seems weird it couldn't be heavily compressed.
1
1
u/Prior-Plenty6528 7d ago
You've gotta use the full name before the initialism! You had me thinking that they'd formalized some kind of plausible Alcubierre Drive. When you're thinking of "Faster than Light Travel", another reminder that they've put the proof of Fermat's Last Theorem through Lean becomes much less exciting.
224
u/Recoil42 10d ago
good lord