With 13 Million Lines of Code in 11 Days, Claude Crafts Fermat's Last Theorem

Anthropic announced that the AI model "Claude" managed, in a semi-independent manner, to formulate Fermat's Last Theorem as computer code within 11 days.

This resulted in approximately 13 million lines of code in the "Lean" language and about 29,500 intermediate theorems, equivalent to roughly five times the size of the entire official mathematics library "Mathlib".

It should be noted that French mathematician Pierre de Fermat proposed the theorem in the 17th century, but its proof remained elusive for over three centuries until British mathematician Andrew Wiles finally proved it in 1995, after working on it in secret for nearly seven years.

The formalization means translating the mathematical proof into computer code, enabling computers to verify the correctness of each step.

Many mathematicians attempted to find a proof for this problem, but their efforts ended in failure. Wiles worked on the problem in secret for seven years before announcing a major breakthrough in 1993. Mathematical proofs often consist of long chains of logical reasoning, where some steps depend on others; thus, an error slipping into one step could collapse the entire proof.

This is exactly what happened with Wiles when a flaw was discovered in his proof, taking nearly a year to fix.

Formalizing mathematical theories—digitizing them—transfers them from the world of "pen and paper" to the realm of computer code, allowing computers to process and verify their logic step by step, uncovering any errors or vulnerabilities. The central repository "Mathlib" contains approximately two million lines of formally written mathematics.

Professor Kevin Buzzard from Imperial College London spent five years completing this task, while the "Claude" model achieved it in just 11 days. According to Buzzard, the proof "relies on nothing except mathematical axioms".

The task was divided among AI agents receiving general instructions periodically, with the tool "Prove2Me" helping coordinate their work. It was originally designed to assist human mathematicians.

If these results prove reliably reproducible, AI could accelerate the translation of modern mathematics into machine-verifiable formats.