Formalizing Fermat's Last Theorem

kdavis

Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT

lalitmaganti

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.

andrewla

Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/

kristjansson

Well, time to set down the glass beads and dive into a an alpine lake.

rao-v

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!

m_w_

> 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.

Vakaiser

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.

lseplot

https://github.com/anthropics/fermats-last-theorem/blob/main... status: "self-assessed" 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!

aaraujo002

They released the code here: https://github.com/anthropics/fermats-last-theorem

sigmar

>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.

baggy_trough

I won't be impressed until it identifies the proof he wrote in the margin. /s

jrflo

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

atleastoptimal

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.

somberi

On a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

bluecalm

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!

anony-123

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?

drivebyhooting

LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?

estetlinus

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.

KaiserPister

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

kzrdude

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?