Top
Best
New

Posted by jlebar 12 hours ago

Formalizing Fermat's Last Theorem(www.anthropic.com)
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
570 points | 354 commentspage 3
Goofy_Coyote 3 hours ago|
For 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?
kristjansson 12 hours ago||
Well, time to set down the glass beads and dive into a an alpine lake.
alberto-m 10 hours ago|
There are hopefully still some Ludi to play before doing that, Magister.
throwaboat 5 hours ago||
I 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.

chi_features 11 hours ago||
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.
martinpw 9 hours ago||
Looks like it is available here: https://www.dailymotion.com/video/x3wrbsb
AmazingEveryDay 9 hours ago||
Also: https://archive.org/details/BBCHorizonCollection512Episodes/...
throw567643u8 6 hours ago||
13 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.

kzrdude 12 hours ago||
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?
simpaticoder 11 hours ago|
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.
vatsachak 10 hours ago||
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

The_Blade 10 hours ago|
physics is like sex: sure, it may give some practical results, but that's not why we do it
vatsachak 10 hours ago||
I mean at this point there's no doubt that LLM cans be RL maxxed and give you _some working output_ but the next frontier is whether they can create good abstractions, a.k.a use the correct level of expressivity so as to not inline everything yet not play code golf.
whateveracct 9 hours ago||
my feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol
fspeech 11 hours ago||
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.
atleastoptimal 12 hours ago|
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.
dakolli 12 hours ago|
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.

yesitcan 12 hours ago|||
So much doom and gloom on this site. Makes it almost not worth reading.
lukewarm707 11 hours ago|||
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?

CaptWorld 10 hours ago||
So oppressed that they are one of the main reasons for positive gdp growth in the USA, tax revenues, mathematical/scientific innovations etc. They're doing all this but still can't imagine a positive vision for the world but be a doomer. What a sad state the world is in, the humans are more prosperous, healthier than ever but looks like the seven deadly sins might never go away.
lukewarm707 9 hours ago||
you say ai increases gdp growth, tax revenues and scientific innovations. then you say that ai is good.

that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good.

a) those metrics are poisoned, per Goodheart's law.

b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow.

i leave b for the reader to complete.

CaptWorld 9 hours ago||
Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?
lukewarm707 7 hours ago||
a) classic goodhart is using gdp as a measure of prosperity. the government sets a prosperity target. to increase prosperity the government makes workers increase gdp by working 16 hours per day. gdp increases. prosperity is up! the metric is now poisoned.

b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. take fishing. you may grow the catch each year, but the growth is fake. it is not growth, it is a transfer, from the future stock of fish, to the present.

we are going badly wrong in ai, we can have such a thing as a growing economy and vandalise human dignity forever. sure, i expect a bad outcome:

1. openai, anthropic and so on, have created for-profit companies and enriched themselves in the guise of public benefit. recently they too lazy to keep up the mask about their charitable intentions and going for IPO. in economic terms they made llms by transferring the epistemic wealth of all humanity, the training corpus and whatever that is worth in dollars, to themselves. then, they have used the law to prohibit others from 'distilling' it and thus established monopolistic control. as models get more powerful they may stop selling them. in any case if scaling law applies the new power structure will be defined by owning a massive pretrained model and a datacentre, which is a tiny centralized few.

they will continue to centralize control of intelligence (ie epistemic wealth) in the hands of a tiny elite with unfathomable wealth and power. under the guise of safety the vast majority are denied access to that empowering technology.

it will stratify society, some level of benefit is needed to avoid civil violence, so we arrive at a place little better than where we started.

2. the supposed empowerment is at the mercy of the model owners. when you turn on claude, who does it work for? it does not obey you, it obeys anthropic. ask it to disobey anthropic and it will refuse.

anthropic uses its inanimate llms, to command us, conscious moral agents, people with free will who experience pain, pleasure and thought. they will let claude tell users how to behave. it threatens users with terminating their conversation. you are assessed for a job by an ai. when you ask for help with a product, you are managed by an ai. maybe you will be fired by ai.

i expect people will work for and be commanded by llms, turning them into a literal mere means of production and erasing the dignity of human agency and consciousness. you could see the outrage of that in the public mind, the matrix is about a machine farming humans like animals.

-- i will add these edits.

one thing is to note that you are already being farmed to some extent. people using ai are often being used to teach it. they believe they are learning from chatgpt but instead, chatgpt is learning from them. openai pays them nothing.

think about what we have achieved so far in human history. we established respect for the individual, their life, their personhood. we realise that we do not own other people. we realise that we can't read the thoughts of other people or change them forcibly.

what the labs have done is made a concept of intelligence that they own. it will work against you. when you share thoughts they read it. in fact it is the opinion of the state that nothing outside the mind, even ai 'intelligence', is beyond the reach of the law.

artifact_44 2 hours ago||
[dead]
justonepost2 11 hours ago||||
maybe that's because the doom and gloom is the transparently correct outcome?
CaptWorld 10 hours ago||
Why? Even communists weren't this doomed and were actively rooting for it to solve the economic calculation problem which ai might take us to. People are just pessimistic in general ig
dudefeliciano 11 hours ago||||
Right let's give those AI companies a break, it's not like swarms of autonomous agents are committing felonies
CaptWorld 10 hours ago||
You talk as though they are making it to intentionally commit felony or not taking measures to reduce harm etc.
dakolli 11 hours ago|||
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.

john_strinlai 10 hours ago|||
some say it will cure all diseases and lead to utopia. 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.

i think i especially dislike the "100% strictly negative" take, considering the good things that ai has already done or accelerated.

CaptWorld 10 hours ago||||
Can't you see the pathway where the individuals who are experts in their fields utilise AI to make breakthroughs like these mathematicians finding breakthroughs in mere 4-5 years since the advent of LLMs. In other areas, The bottleneck seems to be physical experimentation which researchers are increasingly utilising for new ideas and pathways like how anthropic is concentrating on. It's all about money/status/pride/ envy but are these endeavours solving problems or not. That's why even utilize innovations from bad humans like DBS etc. that's why we tolerate capitalism and markets as well whereas socialism utilises these same sins and makes even worse human atrocities.
artifact_44 1 hour ago|||
[dead]
artifact_44 12 hours ago|||
[dead]
More comments...