Anthropic's AI Formally Proved Fermat's Last Theorem in Lean

Kevin Buzzard, the mathematician leading the Xena project on the formalization of mathematics, reported on his blog: one of Anthropic's internal models, running on the prove2.me platform, has built a complete formalization of the proof of Fermat's Last Theorem (FLT) in the Lean language. This closes the last, hitherto unassailable item on Freek Wiedijk's famous list of a hundred formalization challenges — a benchmark that is now twenty years old.

What exactly has been proved

The model formalized not the “modern” proof that Buzzard himself is working on, but the classical version — the Darmon–Diamond–Taylor exposition of 1995 of the Wiles–Taylor argument, via the Langlands–Tunnell theorem and Ribet's level-lowering theorem. The repository develops the theory of Fontaine and a sufficient portion of Mazur's work on the Eisenstein ideal. Formally the proof works for primes p ≥ 5, but this is not a gap: for odd regular primes FLT had already been formalized earlier (Best–Birkbeck–Brasca–Rodriguez), and the smallest irregular prime is 37. So every case is covered.

The scale is impressive: over 13.4 million lines of code, with compilation taking nearly twenty times longer than the mathlib mathematical library — even on a machine with 96 cores and 500 GB of RAM. Buzzard personally built the code and ran the comparator verifier — it checks out.

The work is not over

Buzzard himself is funded by an EPSRC grant (a million pounds over five years) precisely for the formalization of FLT, and the first thought is that there is now nothing left for him to do. But that is not so. Anthropic formalized the old proof in its entirety; the researcher, however, promised his funder something else: first, to contribute the fundamental objects of modern number theory to mathlib, and second — more importantly — to create a “living document” that lets people explore the modern proof. Anthropic is unlikely to take that on: for them the task is done.

Mathematically, the author admits, the result says almost nothing new — the community was already confident in the proof's correctness. What it does show is what is possible in autoformalization: if a machine verifies thousands of pages of literature in eleven days, then before long the formalization of fresh research will become routine, and the reviewing of papers far less painful. Machines will ruthlessly flag the gaps in arguments that are “known to the experts” and force authors to be more honest.

The comments cite a curious figure: according to Anthropic, the proof cost 6 billion output tokens — about 300 thousand dollars at API rates. Buzzard himself notes wryly: he was given a million for five years, the company managed it in eleven days, but probably spent more.

He closes with a personal anecdote: he learned of Wiles's 1993 proof late, having gone off on holiday to Ireland; and now the letter from Anthropic reached him at a music festival in Wales — a message with the subject line “End-to-end Lean formalization of Fermat's Last Theorem” that he at first took for spam from some crank.

Source: Lobsters