Anthropic says it has produced the first complete computer-checked proof of Fermat’s Last Theorem, with Claude working largely autonomously for 11 days to formalize the result in Lean. If confirmed and widely replicated, the work would be a significant marker for both mathematics and AI-assisted research.
Fermat’s Last Theorem is one of the most famous statements in mathematics: no positive integers a, b, and c satisfy aⁿ + bⁿ = cⁿ for any integer n greater than 2. Andrew Wiles first proved the theorem in 1995, but the proof remained an informal human argument that still required expert verification. The long-running project described by Anthropic aimed at something different: not a new proof in the ordinary sense, but a machine-checkable formalization of the existing mathematical chain.
That distinction matters. A formal proof can be independently verified by a computer kernel, which reduces ambiguity and helps catch subtle errors. The Lean proof assistant is one of the main tools in that ecosystem. According to Anthropic, Claude translated a large body of mathematical reasoning into Lean code and reached a version that the company says checks fully and matches the theorem statement in the formal library.
The claim is notable on two levels. First, it suggests that frontier models are becoming capable of sustained work over highly structured technical domains. Second, it shows that AI systems may soon be useful not just for suggesting ideas, but for assembling large, verifiable artifacts that humans can inspect and trust. Anthropic says the project produced thousands of theorems along the way and involved an extensive proof development effort rather than a single clever leap.
The Lean community has been working toward a formalization of Fermat’s Last Theorem for years, with Kevin Buzzard’s project playing a central role. The point of that work has never been to replace mathematics with automation. Instead, it aims to make difficult results more auditable and to improve the infrastructure used for future work. Anthropic’s announcement arrives in that context, not outside it.
Independent Lean community pages and the project repository confirm that FLT formalization has been a live, multi-author effort. Those materials establish the broader research program even if they do not by themselves verify the exact scope of Claude’s contribution. Taken together with Anthropic’s announcement, they show that this is not a random demo but a result plugged into an active mathematical project.
The news is still early. A company announcement is not the same thing as a detailed peer-reviewed mathematics paper, and the research community will want to inspect the proof, the tooling, and the assumptions carefully. But even that caution does not erase the significance. If a general-purpose model can work through a formal proof of this scale, it suggests a new stage for AI in mathematics: one where the output is not just persuasive text, but a reproducible object that a machine can check.
That possibility matters far beyond Fermat’s Last Theorem. The same methods could eventually apply to large libraries of mathematics, formal verification of software, and any domain where trust depends on exact symbolic reasoning. Anthropic’s announcement is best understood as a milestone on that path, not an endpoint. It shows what can happen when a model is asked not merely to explain a theorem, but to build a proof that a computer can independently certify.
