An AI System Just Spent 11 Days Reproving One of Math's Most Famous Theorems — And an Outside Mathematician Says It's the Real Deal

Fermat's Last Theorem took over 350 years to prove the first time. Getting a computer to formally verify that proof was expected to take years on its own. It took eleven days.

Anthropic announced this week that its Claude AI system produced the first complete, machine-checked proof of Fermat's Last Theorem in the Lean programming language — a process called formalization, where a mathematical proof gets translated into a form that automated proof-checking software can verify line by line, catching any logical gap a human reviewer might miss.

The scale of what was generated is genuinely enormous. According to Anthropic's own research post, the effort produced 13 million lines of Lean code and proved 30,300 individual theorems, with 29,500 of those directly used in the final proof — a body of work more than five times larger than Mathlib, the primary community-maintained library of formalized mathematics that the project built on top of.

Fermat's Last Theorem itself was first proven by mathematician Andrew Wiles in 1995, more than 350 years after the conjecture was originally proposed. What Anthropic's system did wasn't discover new mathematics — it converted Wiles's existing proof (specifically a simplified version developed by mathematicians Darmon, Diamond, and Taylor) into fully machine-verifiable form, something mathematicians had broadly expected would take years of dedicated human effort.

The technical setup involved dozens of Claude-based agents working through a platform called Prove2Me, built by Anthropic researcher Tianyi Peng's group at Columbia University. According to the company, the agents operated largely autonomously over the 11-day run, generating roughly six billion output tokens, with human input limited mostly to occasional high-level prompts — things like flagging which sub-theorem to prioritize next, rather than any direct mathematical guidance.

Independent verification came from Kevin Buzzard, a mathematician at Imperial College London who has separately worked on formalizing Fermat's Last Theorem himself. Buzzard reviewed Anthropic's proof and, in his own blog post, called it "an extraordinary achievement," noting it proves the theorem "with no assumptions other than the axioms of mathematics" and arrived far faster than experts had anticipated. He went further, suggesting the result signals a meaningful step toward automatic formalization of modern mathematical literature more broadly — a long-standing, difficult goal in the field.

The project wasn't Anthropic's first attempt. According to SiliconANGLE's reporting, an initial effort to formalize Wiles's proof was unsuccessful, and the eventual breakthrough came specifically after the team incorporated Prove2Me into the workflow — underscoring that the achievement rested as much on tooling and infrastructure as on the underlying AI model's raw capability.

Anthropic has also been transparent about attribution. The company's repository credits 106 upstream files to Buzzard's own earlier Imperial College London FLT formalization project, along with broader contributions from the Mathlib community — a detail that matters for how credit gets distributed in an emerging field where AI-assisted results build directly on years of human mathematical groundwork.

Whether this specific achievement translates into faster verification of future mathematical results, or remains a striking one-off demonstration, is still an open question the field will need time to answer. But for a proof that once took Wiles roughly seven years to originally develop and mathematicians years more to fully verify by hand, having a machine-checked version completed in less than two weeks marks a genuinely notable data point in how far automated formal verification has come.

Spotted a story we should dig into? Drop us a line at tips@kanilprwire.com.