Claude's 11-day proof of Fermat's Last Theorem passes computer verification

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

"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. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order p>=17. This means that their FLT proof only works for p>=17, however FLT was already formalized for odd regular primes by Best-Birkbeck-Brasca-Rodriguez, and the smallest irregular prime is 37, so it’s all good."

My question to any mathematician reading this: does the above make ANY sense to you?

I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.

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

> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.

At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.

On a tangential note, I highly recommend this book by Simon Singh.

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

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

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.

Ok, let’s get a rabid pack of agents cranking on P = NP? next!

With how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.