Claude Fully Formalizes Fermat's Last Theorem in 11 Days, Generating 13 Million Lines of Lean Code

Researchers from Anthropic, including Tianyi Peng, and a team from Columbia University successfully used Claude to fully formalize Fermat's Last Theorem (FLT) in the Lean programming language. The process was largely autonomous over approximately 11 days, ultimately producing 13 million lines of Lean code and 29,500 proven intermediate lemmas. This is more than five times the size of the existing community library Mathlib, making it one of the largest computer-verified proofs in mathematical history.

The Role of the Multi-Agent Collaboration Platform 'Prove2Me'

To achieve successful formalization, the research team used an open collaboration platform called Prove2Me. This platform provides the following features to enable multiple Claude agents to collaborate effectively:

• DAG Maintenance: Managing the Directed Acyclic Graph (DAG) of theorem statements to prevent memory degradation between agents and enable parallel work.
• File Separation Strategy: Separating theorem statements from proofs and maintaining links independently to improve Lean compilation speed and minimize resource consumption.
• Natural Language Descriptions: Maintaining natural language descriptions for each theorem to derive simpler proof paths through search and reuse.

Initial attempts saw failures such as agents losing track of the project state, but after adopting Prove2Me, dozens of agents resolved the problem by dividing tasks from concept definition to proving complex propositions. Human intervention was limited to high-level instructions.

A New Paradigm in Mathematical Verification

This achievement demonstrates AI's ability to algorithmically verify complex mathematical logic. Kevin Buzzard (Imperial College London) evaluated this work as a major step toward the automatic formalization of modern mathematical literature. Formalized proofs are expected to become a key tool for reducing errors in complex logical chains that are difficult for humans to understand and ensuring the reliability of AI-generated mathematical results.

Additionally, Anthropic researchers successfully completed the formalization of Vinogradov's Three Primes Theorem in just 3 days using three personal Claude Max plans. This suggests that with appropriate scaffolding and a collaboration platform, major mathematical results can be formalized even with consumer-grade AI subscriptions. In the future, such technology is expected to contribute to eliminating errors in mathematical knowledge bases and reducing the burden of reviewing new research.