Anthropic completes the first end-to-end verified formalization of Fermat's Last Theorem

Anthropic announced (9/4) the first complete, end-to-end computer-verified proof of Fermat's Last Theorem in Lean, using only Lean's three standard axioms and following the Darmon–Diamond–Taylor modularity route rather than the full Wiles proof. The work was 'largely autonomous' over 11 days: about 13 million lines of Lean (over 5x the size of Mathlib), 29,500 intermediate theorems, and roughly 6 billion output tokens, orchestrated through the Prove2Me parallel proving platform (Columbia, Tianyi Peng's group) on top of a Claude Code multi-agent framework, driven by an internal research model roughly comparable to Claude Fable 5.1. A second experiment formalized Vinogradov's three-prime theorem in 3 days using three Claude Max accounts. Kevin Buzzard (Xena project), who reviewed the effort, endorsed the result — Anthropic 'beat him to it.' The code is public at github.com/anthropics/fermats-last-theorem. HN front page at 442+ points.

This is the strongest public demonstration yet that agentic AI plus a verification loop can complete a formalization task that has sat open for decades — and the recipe generalizes beyond math: draft, run the checker, feed errors back, parallelize across agents. Any team doing formal verification (protocol proofs, kernel invariants, spec conformance) can copy the orchestration pattern today; the repo is the reference implementation. It is also the highest-profile real workload yet run on the multi-agent runtime pattern this KB tracks as trend #3.