Claude Completes First Formal Proof of Fermat's Last Theorem in 11 Days

On September 4, Anthropic announced that its Claude AI model, guided by minimal human input, completed the first full formal proof of Fermat Last Theorem in just eleven days. Initiated by Tsinghua University alumni and researcher Tianyi Peng, the project leverages a multi-agent framework built on the Lean proof assistant to translate Andrew Wiles and Richard Taylor 1995 mathematical proof into machine-verifiable code. The formalization required generating approximately thirteen million lines of Lean code and proving over thirty thousand intermediate lemmas, of which roughly twenty-nine thousand five hundred constitute the final argument. Executed across dozens of concurrent Claude agents, the workflow initially struggled with state management and dependency tracking. The team resolved this by deploying Prove2Me, a specialized collaboration platform that decouples theorem statements from their proofs and maintains a dynamic dependency graph. This architecture enables parallel proof generation while preserving logical integrity, allowing the system to navigate complex number-theoretic components such as Frey curves, modularity lifting, level lowering, and the R=T correspondence. Verification was rigorously enforced. The final proof depends solely on three foundational logical axioms within Lean, avoiding any unproven assumptions. To ensure accuracy, Anthropic deployed a comparator to align the final proposition with Mathlib standards and subjected the entire environment to an independent, Rust-based core verifier named nanoda. The independent check accepted over 1.05 million declarations, confirming the logical consistency of the derivation. Despite the computational success, the project highlights significant engineering challenges. The generated codebase exceeds Mathlib current size by fivefold, primarily because machine-generated proofs prioritize verifiability over conciseness and human readability. Substantial manual refactoring will be required to optimize the code, standardize definitions, and extract reusable mathematical modules. The initiative consumed approximately six billion output tokens and required roughly 153 gigabytes of peak memory during construction, alongside extensive verification processes. While Anthropic has not disclosed the total financial cost or comparative efficiency against human-led formalization, the experiment establishes a new benchmark for AI-driven mathematical engineering. It demonstrates that large-scale, centuries-old proofs can be systematically decomposed, parallelized, and computationally verified, offering a scalable template for future AI-assisted research. Nevertheless, bridging the gap between machine-verifiable derivations and human-interpretable mathematics remains an active frontier, underscoring that formal correctness and mathematical utility are currently distinct engineering objectives.