Anthropic: Claude formalizes Fermat’s Last Theorem in Lean

4 Sep 2026: Anthropic published “Formalizing Fermat’s Last Theorem,” saying Claude produced the first complete computer-checked proof of FLT in Lean after working largely autonomously for about 11 days — ~13 million lines of Lean and ~29,500 intermediate theorems on Anthropic’s figures. Company research post is the primary. This is a verification/autoformalization story, not a claim that Wiles is superseded or that a Clay prize was awarded.

4 Sep 2026: Anthropic published “Formalizing Fermat’s Last Theorem.” The company says Claude produced the first complete computer-checked proof of Fermat’s Last Theorem in Lean. That dated research post is the filing event.

Anthropic: Claude worked largely autonomously for about 11 days and produced the first end-to-end, computer-checked FLT proof in Lean. Those are the company’s claims — not an independent audit of autonomy.

Anthropic’s figures on the same page: 13 million lines of Lean; 29,500 intermediate theorems in the final proof; 30,300 theorem proofs along the way; more than 5× the size of Mathlib. Those are company figures. This desk did not recount the repo.

Anthropic says the proof follows a simplified version of Wiles’s path from Darmon, Diamond, and Taylor. Human mathematical input, on the company’s account, was limited to occasional high-level instructions from Tianyi Peng, an Anthropic researcher whose Columbia group builds AI formalization tools.

The finished proof was checked by Lean, Anthropic says; it uses Lean’s three standard axioms, and a comparator confirmed the statement matches Mathlib’s own statement of FLT. Treat the Lean check and the comparator as Anthropic’s verification claims.

The effort succeeded after switching to Prove2Me — an open collaborative formalization platform designed by Tianyi Peng and Columbia collaborators — which Anthropic says kept a DAG of theorem statements, split statement and proof files, and attached natural-language descriptions for search. Earlier attempts failed; Anthropic says those failed efforts contributed about 7% of the non-boilerplate lines in the final proof.

Kevin Buzzard, quoted on the page: the autoformalization “proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics,” that the artefact is “multi-layered” and “robust enough to be built upon,” and that if FLT autoformalization is possible now, “we have taken a big step towards automatic formalization of the modern mathematical literature.” Those are Buzzard’s comments as published by Anthropic.

Anthropic frames the novelty as verification — checking a known proof the way a calculator checks a computation — not novel mathematics like recent AI-driven Riemann hypothesis work. This is not a new human proof of FLT, and it does not supersede Wiles. FLT is not a Clay Millennium Prize problem; no Clay prize was awarded.

Optional attributed on the same post: the run consumed about six billion output tokens from a general-purpose internal research model Anthropic says is roughly comparable to Claude Fable 5.1; the full proof is on GitHub (anthropics/fermats-last-theorem); acknowledgments name the Imperial College London FLT project, flt-regular, Lean, and Mathlib.

Autoformalization of a historic theorem at Lean-checkable scale — verification with dated Anthropic receipts, not a new human FLT proof or Clay award.