AI 研究／形式驗證
Claude Uses Multi-Agent Collaboration to Formalize Fermat’s Last Theorem in Lean, Releases 13-Million-Line Proof
Anthropic says dozens of Claude agents completed the first fully computer-checkable, end-to-end proof of Fermat’s Last Theorem in 11 days. The real breakthrough lies not only in model capability, but in how Prove2Me uses theorem dependency graphs, independent compilation, and search mechanisms to manage long-running collaboration.
Anthropic has released a formal proof of Fermat’s Last Theorem written in Lean 4. According to its [technical report](https://www.anthropic.com/research/formalizing-fermats-last-theorem), dozens of Claude agents worked through the Claude Code multi-agent framework for 11 days, generating approximately 13 million lines of Lean and proving 30,300 intermediate theorems, about 29,500 of which were ultimately used. The reasoning model was an internal research version with capabilities roughly equivalent to Claude Fable 5.1, and the project consumed about 6 billion output tokens.
Early attempts failed because the agents gradually lost track of the project state and could not effectively reuse previous results. The team switched to Prove2Me, which decomposes the goal into a directed acyclic graph. Agents can select unfinished theorems, search existing results, and compile theorem declarations separately from their proofs, avoiding the need to reprocess the entire proof tree whenever a single node changes. The [Prove2Me paper](https://arxiv.org/abs/2608.28433) describes the architecture as a collaborative formalization platform designed to accommodate both humans and agents.
The public [proof repository](https://github.com/anthropics/fermats-last-theorem) pins Lean 4.33.1 and Mathlib 4.33.0 and prohibits escape hatches such as `sorry`, additional axioms, and `unsafe`. After the Lean kernel completes a full build, `comparator` further verifies that the final proposition matches the one in the corresponding Mathlib version. A separate kernel called nanoda, implemented in Rust, also checks more than 1.05 million declarations. The proof relies only on three standard Lean axioms.
Claude did not discover a new proof of Fermat’s Last Theorem. Instead, it converted the approach developed by Frey, Serre, Ribet, Wiles, and Taylor–Wiles into a machine-verifiable artifact. Reproducing the result is also expensive: Anthropic’s full build used 153 GB of memory, while `comparator` took about 15 hours and peaked at 230 GB. Kernel checking can guarantee type correctness, but it cannot determine whether the names of intermediate theorems faithfully reflect their mathematical meaning. The next questions are whether independent teams can reproduce the result and whether this orchestration method can handle other large bodies of mathematical literature with fewer tokens and less human prompting.