Agent Horizon

Anthropic published a research post describing how an internal, unreleased version of its Claude model produced what the company calls the first complete, computer-checked formalization of Fermat’s Last Theorem in the Lean proof assistant. According to Anthropic, the model worked largely autonomously over 11 days, writing roughly 13 million lines of Lean code and proving around 29,500 to 30,300 intermediate theorems along the way, based on a simplified version of Andrew Wiles’s 1995 proof. Imperial College London mathematician Kevin Buzzard, who leads a multi-year community effort to formalize the same theorem, reviewed the artifact and confirmed it holds up using only the standard axioms of mathematics.

What actually happened here

It’s worth being precise about what this is and isn’t. Fermat’s Last Theorem was proven by Andrew Wiles three decades ago — nobody is claiming new mathematics was discovered. What Claude did was translate an existing, trusted proof into a form a computer can check line by line, which is a laborious, unglamorous task that the formal-methods community had scoped as a multi-year project with funding running through 2029. Anthropic getting there in 11 days, largely unsupervised, is the real story: it’s a demonstration of sustained, self-correcting, multi-step agentic reasoning on a problem where there’s no room to bluff, because Lean’s compiler either accepts a proof step or it doesn’t.

This lands one month after Anthropic’s other headline math result, where an unreleased Claude model pushed a technical bound related to the Riemann Hypothesis from 41.6% to 67.2% — a genuine but narrower improvement that the company was careful to say wouldn’t lead to solving the hypothesis itself. Taken together, these two releases suggest Anthropic is deliberately building a track record of machine-checkable research artifacts rather than leaning on benchmark tables, which is a healthier way to make capability claims than most of the industry currently uses.

For developers and researchers, the practical takeaway is narrower than the headlines: this isn’t a product feature you can access today, since the model involved is an internal research version, not a shipping Claude release. The genuinely useful signal is that autoformalization tools like the Prove2Me platform used here are maturing fast enough that AI-assisted verification could plausibly start reducing the backlog of unrefereed mathematical proofs, a problem that’s been growing as more proofs get produced than the community can check by hand.

The caveat worth keeping in view is scale versus difficulty. Anthropic and outside commentators have both noted that formalizing an already-proven, well-understood result is a different kind of hard than discovering new mathematics — the Riemann work required more creative search per token spent, even though it produced a far smaller artifact. It’s a genuinely impressive engineering and reasoning achievement, but it’s proof-checking infrastructure, not a new theorem, and framing it as anything more would be exactly the kind of overstatement we try to avoid here.