News · 2026-09-05

Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery

Anthropic has released a Lean formalization of a complete classical proof route for Fermat's Last Theorem, and mathematician Kevin Buzzard says the code compiles and checks. The result is a major advance in autoformalization, but it is not an AI discovering a new theorem or independently reinventing the mathematics from scratch.

Key facts

• Anthropic published a research announcement and public Lean repository.
• Kevin Buzzard writes that the artifact formalizes a complete proof and that he compiled it and ran a comparator.
• Buzzard says the route follows the Darmon-Diamond-Taylor exposition of the Wiles/Taylor-Wiles argument.
• He estimates the end-to-end formalization involved thousands of pages and took about 11 days.

Fermat's Last Theorem says that the equation x to the n plus y to the n equals z to the n has no positive-integer solutions when n is greater than two. Andrew Wiles's proof, completed with Richard Taylor, is one of the landmarks of modern mathematics. A Lean formalization is not a narrative explanation of that proof. It is a program-like object in the Lean proof assistant whose every step is checked against formal definitions and rules.

Buzzard is unusually well placed to scope the result because he leads related formalization work. In his post, he says Anthropic's internal model, through prove2.me, 'formalized a complete proof of Fermat's Last Theorem (FLT) in Lean.' He adds, 'it checks out,' after compiling the code and running a comparator. He says he also inspected every non-mathematical line for malicious material. That is substantially stronger confirmation than a launch benchmark.

The precision matters. Buzzard says this is not the modern proof route his own project has been formalizing. It follows an early Darmon-Diamond-Taylor exposition using Langlands-Tunnell and Ribet. The repository develops enough Fontaine theory and Mazur Eisenstein-ideal machinery to rule out relevant Frey curves for p at least 17; other pieces were already present. So the theorem statement is fully formalized, while the mathematical content remains existing literature.

An analogy helps. Translating a classic novel into a language with an unforgiving compiler does not write a new novel. It proves that the translation preserves every sentence under strict grammatical rules, and it creates a version future readers can mechanically check. The difficult part is that mathematics contains definitions, library dependencies and tacit conventions that humans handle informally. Turning thousands of pages into verified Lean code is a substantial systems and reasoning achievement.

Buzzard is careful not to overclaim. He says the artifact 'tells us essentially nothing' mathematically because it adds no new theorem content. His own EPSRC-funded work still needs contributions to Lean's math library and a dynamic, human-readable document so mathematicians can explore the proof. A formal artifact can be correct and still be difficult for a human to maintain or learn from.

That is the best counterargument to triumphalist headlines: autoformalizing an established proof is not the same as creating mathematics. The response is not to minimize the result, but to name it correctly. It demonstrates that an AI-assisted system can produce a complete, independently checkable formal artifact at a scale that was recently implausible. That may make mathematical review, collaboration and assumption-checking more rigorous. It will not eliminate the need for people who know what result is worth proving and why. For background, see what a proof assistant is.

Primary source, verified: read the paper →

Ground Truth. (2026, September 5). Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery. Ground Truth. https://groundtruth.day/news/anthropic-lean-formalizes-fermats-last-theorem.html

@misc{groundtruth:anthropic-lean-formalizes-fermats-last-theorem,
  title  = {Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/anthropic-lean-formalizes-fermats-last-theorem.html}
}

Topics: mathematics · formal-verification · lean · anthropic · research