Anthropic 'formalizes' Fermat's Last Theorem like never before using Claude but it still took 11 days to write out

Date:
Sun, 13 Sep 2026 15:15:00 +0000

Description:
Anthropic says Claude formalized Andrew Wiles proof of Fermats Last Theorem
in 11 days, producing 13 million lines of Lean code.

FULL STORY ======================================================================Copy link Facebook X Whatsapp Reddit Pinterest Flipboard Threads Email Share this article 0 Join the conversation Follow us Add us as a preferred source on Google Newsletter Subscribe to our newsletter Claude turned a famous mathematical proof into millions of checkable code lines Anthropic says
Claude completed years of expected work in 11 days The massive proof contains 13 million lines of Lean code Anthropic has used its Claude artificial intelligence system to produce a fully computer-checked version of a famous, centuries-old mathematical proof.

The proof addresses Fermat's Last Theorem, a hypothesis first proposed by the mathematician Pierre de Fermat back in the year 1637. Mathematician Andrew Wiles produced the very first full mathematical proof of the theorem back in 1995, spanning 129 pages total in length. Latest Videos From TechRadar Watch full video here: A proof rebuilt for machines Formalizing a proof simply
means converting its mathematical reasoning into code that computers can
check automatically without any human assistance.

Anthropic says it expected the entire task to take several years, based on how mathematicians first described the project. You may like Anthropic launches "AI workbench" for scientists using Claude Claude Sonnet 5 is here, and it's the 'most agentic Sonnet model yet' Samsung thinks Claude Code can help it boost chip design but admits the AI still makes some worryingly big mistakes

Instead, the company says its internal research model finished the entire proof in only 11 days of continuous, largely unsupervised work.

The finished proof runs to 13 million lines of specialized code written in a programming language called Lean, used by mathematicians. Are you a pro? Subscribe to our newsletter Sign up to the TechRadar Pro newsletter to get
all the top news, opinion, features and guidance your business needs to succeed! Contact me with news and offers from other Future brands Receive email from us on behalf of our trusted partners or sponsors By submitting
your information you agree to the Terms & Conditions and Privacy Policy and are aged 16 or over.

Along the way, Claude's agents reportedly proved roughly 30,300 separate theorems, ultimately using 29,500 of them in the final version.

Human input was reportedly limited to occasional high-level guidance, rather than any direct hands-on coding throughout the entire eleven-day process.

At 13 million lines, the resulting proof is over five times larger than Mathlib, the community's own main proof library. What to read next Claude
will now hide an invisible watermark inside ordinary words Claude was down
for many Anthropic says the outage is now 'resolved' Claude can now enter all your passwords for you - if you give it permission

"This extraordinary autoformalization achievementproves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," said Kevin
Buzzard, a mathematician at Imperial College London.

Along the way we see autoformalization of algebra, harmonic analysis,
geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.

Anthropic attempted the formalization several times before succeeding, with those efforts contributing roughly 7% of the final proofs non-boilerplate lines. Not Anthropic's first math breakthrough The formalization arrives just one month after Anthropic detailed a separate breakthrough involving the Riemann zeta function, a well-studied mathematical object.

That function sits at the very center of the Riemann hypothesis, considered one of mathematics' hardest unsolved problems worldwide.

Rival lab OpenAI is also pursuing similar work, using its newest Astra model to solve several classic Erds problems.

That same OpenAI effort also reportedly narrowed several long-standing open questions within the field of theoretical computer science.

Anthropic says its breakthrough came only after giving Claude access to an open-source software tool named Prove2Me, built by outside collaborators.

The software helps AI agents pick the most useful next step during a long, multi-stage research workflow, while also cutting inference costs.

Anthropic has also expanded free access and research credits for mathematicians working specifically on formalization projects, alongside dedicated larger grants.

Despite the record pace set here, an eleven-day timeline still shows how labor-intensive full formalization remains, even with today's most capable systems. Follow TechRadar on Google News and add us as a preferred source to get our expert news, reviews, and opinion in your feeds.



======================================================================
Link to news story: https://www.techradar.com/pro/anthropic-formalizes-fermats-last-theorem-like-n ever-before-using-claude-but-it-still-took-11-days-to-write-out


--- Mystic BBS v1.12 A49 (Linux/64)
* Origin: tqwNet Technology News (1337:1/100)