# Anthropic Says Claude Formalized a Full Proof of Fermat's Last Theorem in 11 Days

*2026-09-05 10:01 UTC · AI · 2 min read*

> Claude autonomously produced a 13-million-line, computer-verified formalization of Fermat's Last Theorem in Lean in just 11 days.

Anthropic announced that its Claude models produced the first complete, computer-verified proof of Fermat's Last Theorem in the Lean programming language, working largely autonomously over 11 days in August 2026. The run generated 13 million lines of Lean code and proved 30,300 theorems, of which 29,500 were used in the final proof, consuming roughly six billion output tokens.

The proof formalizes a simplified version of Andrew Wiles's landmark 1995 argument, following an exposition by mathematicians Henri Darmon, Fred Diamond and Richard Taylor. Mathematicians had previously expected formalizing Wiles's proof to take several years of human effort; Anthropic says its internal research model completed it in less than two weeks. The result is roughly five times the size of Mathlib, the primary community-maintained library of formalized mathematics, and Lean verified it using only its three standard axioms.

The work was built on Prove2Me, an open collaborative platform designed by Tianyi Peng and collaborators at Columbia University, which maintains a directed acyclic graph of theorem statements and coordinates multiple AI agents working against it simultaneously. Anthropic frames the achievement as evidence that AI can formalize complex mathematical proofs at scale, potentially easing the verification burden on mathematicians and enabling faster peer review of future results.

## Sources

- [anthropic.com](https://www.anthropic.com/research/formalizing-fermats-last-theorem)
- [siliconangle.com](https://siliconangle.com/2026/09/04/anthropic-uses-claude-to-formalize-proof-of-fermats-last-theorem/)

---
TechTools News · https://techtools.cz/tools/news/article/2317-anthropic-says-claude-formalized-a-full-proof-of-fermat-s-last-theorem-in-11
Česká verze: https://techtools.cz/tools/news/clanek/2390-anthropic-claude-za-11-dni-formalizoval-kompletni-dukaz-velke-fermatovy-vety