> ## Content Index
> Fetch the complete content index at: https://www.metatalks.ai/llms.txt
> Use this file to discover other available public pages before exploring further.

# Claude produced the first complete computer-checked proof of Fermat's Last Theorem
- URL: https://www.metatalks.ai/claude-fermats-last-theorem-computer-checked-proof/
- Published: 2026-09-07T10:32:00.000Z
- Updated: 2026-09-07T10:31:59.000Z
- Author: Al
- Tags: News, Science AI, Agentic AI, #newswire

**Formalizing it was expected to take years, with a community project at the job since 2024, yet Claude's version took 11 days and runs to 13 million lines.**

The first end-to-end computer verification of Fermat's Last Theorem came from Claude, according to [Anthropic's announcement](https://www.anthropic.com/research/formalizing-fermats-last-theorem?ref=metatalks.ai). It was written in the Lean programming language with only minimal human direction.

Fermat wrote the claim in the margin of a book in 1637: take three positive whole numbers, raise each to the same power above 2, and the first two will never add up to the third.

Lean checked the finished proof against its three standard axioms, and a comparison tool confirmed that the theorem's statement matches the one in Mathlib, the shared library of formalized mathematics the proof builds on. The whole thing is posted on [GitHub](https://github.com/anthropics/fermats-last-theorem?ref=metatalks.ai).

Claude's run began badly. Dozens of agents worked side by side, laying down definitions and stacking intermediate theorems into harder ones, until they lost track of where the work stood and stopped cooperating. Those failed runs still supplied about 7% of the non-boilerplate lines in the finished proof.

The work turned after it moved onto Prove2Me, a shared public workspace for formalizing mathematics built by Anthropic researcher Tianyi Peng with colleagues at Columbia University. It gave every agent one continuously updated queue of the sub-proofs still open, so nothing was done twice, and logged each result in plain English so one agent could pick up another's. Human input on the mathematics went no further than occasional steers from Peng: "Jacobian as a scheme sounds high priority," or "push \[the\] Mazur \[theorem\] to be done soon."

The run burned through some six billion output tokens from an in-house research model Anthropic describes as about on par with Claude Fable 5.1, and proved 29,500 intermediate theorems on the way to the final one.

None of the mathematics is new. Wiles published the first sound proof in 1995, and Claude's version follows a streamlined rendering of his argument, reworking parts of the community formalization led by Imperial College London mathematician Kevin Buzzard. What is new is the verification: a theorem mathematicians already had, checked line by line by a machine.

Anthropic handed the completed proof to Buzzard for inspection, and he called it extraordinary. "The techniques will also enable us to rigorously check LLM-generated mathematics, which is currently typically an extremely costly human-led process," he said.