Impressive! Buzzard's group[1] got scooped.

[1] https://github.com/ImperialCollegeLondon/FLT

I suggest also reading Kevin Buzzard's blog post on this as well which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...

Provides great context on this accomplishment and what it means but also doesn't mean.

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

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

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!

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

Stochastic parrots serving Anthropic’s PR department, I’m sure.

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.

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!

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

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

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

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

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.

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

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 a few years later. 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!

We're in the era of slop mathematics. Sure what people are doing is impressive, but how does it make anyonee life better? I still dont see llms as improving our lives here on earth. So far it just seems to make rich people richer and give dopamine hits to nerds (at the cost of everyone's electricity bill).