Anthropic published a research article on September 4, 2026, saying that Claude completed a full computer-checked proof of Fermat’s Last Theorem. According to Anthropic, Claude worked largely autonomously for about 11 days, translating a long proof intended for human readers into a form that the Lean proof assistant could check step by step.
The result is not an AI suddenly discovering an elementary proof unknown to mathematicians. Andrew Wiles published the first correct proof of the theorem in 1995. This project is formalization: rewriting established mathematical reasoning so that a computer can verify its logical structure algorithmically. Anthropic itself frames the novelty as verification rather than as a new mathematical result on the scale of a new Riemann hypothesis proof.
Anthropic says Claude wrote about 13 million lines of Lean and proved 30,300 intermediate theorems, using 29,500 of them in the final proof. The scale makes the formalization burden visible. Human proofs omit steps that readers consider obvious; Lean requires every logical connection to be checkable. Anthropic also says the final artifact is more than five times the size of Mathlib, the main community library it builds on.
The workflow was not a single chat session. Anthropic says dozens of Claude agents collaborated through Prove2Me, using a directed acyclic graph to track theorem statements and working in parallel on definitions, intermediate results, and proofs. That architecture targets a familiar long-running-agent failure mode: memory degradation and loss of project state. Agents need a shared, searchable, reusable proof graph rather than a transcript that only one context window can see.
Lean matters because it checks formal logic, not because a model says that a theorem is proved. Anthropic says Lean checked the finished proof using Lean’s three standard axioms. The post also says Kevin Buzzard reviewed the proof and a comparator confirmed that the theorem statement matched Mathlib’s statement of FLT. Those are useful provenance signals, but this remains an Anthropic research announcement and an open proof artifact. Independent readers should still rerun, inspect, and verify it to their own standards.
For AI-agent research, the case shifts attention from whether a model can produce plausible reasoning to whether a group of agents can maintain state, split dependencies, recover from failure, and deliver a checkable artifact. Anthropic says early attempts failed when agents lost track of the project, and that the effort became reliable only after the shared DAG, faster compilation, and theorem search were introduced.
For mathematicians, a formalized proof does not replace human-readable exposition and does not answer every question about the significance of a result. It is better understood as a reproducible logical foundation. As AI produces more candidate proofs and research hypotheses, shipping a Lean, Rocq, or other proof-assistant artifact alongside the human explanation could become an important way to reduce review burden and catch errors.
The useful headline is therefore not simply that AI proved Fermat’s Last Theorem. It is that agentic research is putting collaboration, formalization, compilation, and verification inside one long-running task. Mathematical novelty, machine checkability, expert review, and independent reproduction remain different things; keeping them separate prevents a valuable verification engineering result from being misreported as AI replacing mathematicians.
