On September 4, Anthropic announced that Claude had completed the first end-to-end, machine-verified formalization of Fermat's Last Theorem. The theorem, first proposed by Pierre de Fermat in 1637, states that no positive integers a, b, and c satisfy aⁿ + bⁿ = cⁿ for any integer n greater than 2. Andrew Wiles finally proved it in 1995 after seven years of secret work—and an additional year fixing a critical gap.
What Claude did was different. It didn't discover a new proof. It translated Wiles' existing proof into a form that computers can check, step by step, with no skipped logic. Mathematicians had expected this formalization project to take years.
13M Lines of Code, 5x Larger Than Mathlib
The numbers are staggering. Claude generated approximately 13 million lines of Lean code—over five times the size of Mathlib, the principal Lean mathematics library. It proved 30,300 machine-verifiable theorems, using about 29,500 in the final proof.
Dozens of Claude agents worked in parallel, defining concepts, proving intermediate theorems, and building toward the final result. The entire effort consumed about 6 billion output tokens from an internal research model roughly comparable to Claude Fable 5.1. Human input was minimal: occasional high-level instructions like "Jacobian as a scheme sounds high priority."
AI Agents Needed a Project Manager—Prove2Me Was the Answer
Claude's first attempts failed. Agents lost track of the project's state and stopped collaborating effectively. The breakthrough came when Anthropic switched to Prove2Me, a platform developed by researcher Tianyi Peng and his collaborators at Columbia University.
Prove2Me solved the coordination problem by maintaining a directed acyclic graph (DAG) of theorem dependencies, allowing agents to see what to prove next. It also separated theorem statements from proofs to speed compilation, and added natural-language descriptions for search and reuse. This was the infrastructure that turned dozens of agents into a functioning research team.
The proof was verified by Lean, using only Lean's three standard axioms, and an independent comparator confirmed the theorem statement matches Mathlib's own formulation of Fermat's Last Theorem.
Autoformalization Just Became a Practical Reality
Imperial College mathematician Kevin Buzzard, who had been leading a separate multi-year project to formalize Fermat's Last Theorem, reviewed Claude's work and confirmed: "I compiled the codebase and ran the comparator on it—the check passed." He noted that the proof leaves "no assumptions other than the axioms of mathematics."
The significance extends beyond Fermat's Last Theorem. Claude's success demonstrates that AI autoformalization artifacts are now robust enough to be built upon. If large mathematical proofs can be formalized in days rather than years, the burden of verifying new mathematical work could drop dramatically. Anthropic suggests that as AI generates more mathematical results, providing formalized versions alongside human-readable proofs may become standard practice.
P.S. The 13 million lines of Lean code are almost certainly longer than necessary—human-written Mathlib is far more compressed. But size isn't the point. The point is that AI agents can now coordinate, prove 30,000 theorems, and produce a machine-checkable proof of one of mathematics' most famous problems—in less time than it takes to read the original 129-page proof. The next question isn't whether AI can formalize math. It's whether humans can keep up with what comes next.
Frequently Asked Questions
Q: What is Fermat's Last Theorem?
A: Fermat's Last Theorem states that no positive integers a, b, and c satisfy the equation aⁿ + bⁿ = cⁿ for any integer n greater than 2. Pierre de Fermat proposed it in 1637, and Andrew Wiles finally proved it in 1995 after 358 years of attempts.
Q: What did Claude actually do?
A: Claude didn't discover a new proof. It formalized Wiles' existing proof—translating it into Lean code that a computer can verify step by step, with no logical gaps or skipped steps.
Q: How long did it take?
A: 11 days. Mathematicians had expected the formalization project to take years.
Q: How much code did Claude generate?
A: Approximately 13 million lines of Lean code—over five times the size of Mathlib, the principal Lean mathematics library.
Q: How many theorems did Claude prove?
A: Claude proved about 30,300 machine-verifiable theorems, using roughly 29,500 in the final proof.
Q: Who led the project?
A: Tianyi Peng, a Tsinghua University alumnus, MIT PhD, Columbia University assistant professor, and Anthropic researcher. Peng also developed the Prove2Me platform used to coordinate the agents.
Q: What is Prove2Me?
A: Prove2Me is a collaborative platform for formalizing mathematics that maintains a directed acyclic graph of theorem dependencies, allowing multiple AI agents to work in parallel without losing track of the project's state.
Q: What was the role of human mathematicians?
A: Human input was minimal—occasional high-level instructions like "Jacobian as a scheme sounds high priority." The actual proof work was handled by the Claude agents.
Q: Was the proof verified?
A: Yes. The proof passed verification by Lean, using only Lean's three standard axioms. An independent comparator confirmed the theorem statement matches Mathlib's formulation. Kevin Buzzard, who leads a separate FLT formalization project, independently confirmed the result.
Q: What is the significance of this milestone?
A: It demonstrates that AI autoformalization is now robust enough to build upon. If large mathematical proofs can be formalized in days rather than years, the burden of verifying new work could drop dramatically.
