On September 4, 2026, Anthropic announced Claude’s result in formalizing Fermat’s Last Theorem—a development relevant to mathematicians working on proof verification. According to the company, Claude produced a proof in the Lean language in 11 days that passed computer verification. The announcement describes completed research.
The result centers on translating mathematical reasoning into a form suitable for automated verification. Anthropic emphasizes that the novelty lies specifically in verifying an already established theorem. The announcement therefore does not mean that Claude was the first to solve Fermat’s mathematical problem.
According to Anthropic’s description, the project used an internal Claude research model. The result applies to that research system; there is no basis for attributing it to a specific publicly available version of Claude.
Practical context: For researchers, the appeal lies in the possibility of obtaining a verifiable formal result alongside mathematical reasoning. This approach could simplify the verification of long chains of deductions. However, a single project does not yet indicate how many resources would be needed to formalize another complex proof.
Sources
Event date: 2026-09-04. Original source date: 2026-09-04.
