Formalizing Fermat's Last Theorem \ Anthropic

Anthropic is an AI safety and research company that's working to build reliable, interpretable, and steerable AI systems.

We are sharing the first complete computer-checked proof of Fermat’s Last Theorem. Claude worked largely autonomously over 11 days to write the proof in the Lean programming language. Below, we describe how the formalization was done and share some thoughts about what this work could mean for research mathematics.Around 1637, Pierre de Fermat jotted down a claim in the margin of his copy of Diophantus’s Arithmetica that would become one of the most famous mathematical conjectures of all time: no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n > 2. Fermat’s Last Theorem (FLT), as the…

saved by

• Gloria Ma
• Florent Tavernier
• Eva L
• Arya G
• Nathan Chen

related reading

• FLT: Anthropic has beaten me to itxenaproject.wordpress.com
• Xena | Mathematicians learning Lean by doing.xenaproject.wordpress.com
• The fall of the theorem economydavidbessis.substack.com
• Announcing FrontierMath Erdősepoch.ai
• 2510.01346arxiv.org
• Mathematics in the Library of Babel - Daniel Littdaniellitt.com
• Human mathematicians are being outcounterexampledxenaproject.wordpress.com
• [2510.01346] Aristotle: IMO-level Automated Theorem Provingarxiv.org
• What's new | Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Taoterrytao.wordpress.com
• startup review: axiom mathil0vemilktea.substack.com
• Computational Complexityblog.computationalcomplexity.org
• Lean Game Serveradam.math.hhu.de