Hacker News front pageSep 5, 2026, 05:00 UTC+8

Anthropic formalized Fermat's Last Theorem in Lean end-to-end

Fermat's Last Theorem: Anthropic has beaten me to it

Anthropic used an internal model and the prove2.me platform to fully formalize Fermat's Last Theorem in Lean. The proof follows the 1995 Darmon–Diamond–Taylor exposition, works only for p≥17, and closes the last item on Freek Wiedijk's 100-theorem list. The codebase is over 13.4 million lines and takes nearly 20× longer to compile than Lean's mathlib. Kevin Buzzard, who is EPSRC-funded to formalize FLT, notes this took Anthropic 11 days versus his 5-year project, but it doesn't produce a human-explorable document or cover the modern proof. He sees it as a milestone for autoformalization, not new mathematics.

Why it matters: Anthropic formalized FLT in Lean, closing the last item on Wiedijk's 100-theorem list — a milestone for the formal-math community. HKR all hit: competitive narrative, concrete technical detail, community resonance. Score capped below 85 because it's pure math with no direct pr...

Read the original ↗Export Markdown

Take

This is worth reading because Kevin Buzzard—the mathematician funded by EPSRC to formalize FLT over five years—wrote the post himself. Anthropic did it in 11 days using an internal model and the prove2.me platform. The proof follows the 1995 Darmon–Diamond–Taylor exposition, works only for p≥17, and combined with prior formalization of odd regular primes, it closes the last item on Freek Wiedijk's 100-theorem list. The codebase is over 13.4 million lines and takes nearly 20× longer to compile than mathlib, even on a 96-core machine.

Don't read this as "AI did new math." Buzzard is explicit: this adds zero new mathematical knowledge—number theorists were already 99.9%+ confident in FLT. The real signal is autoformalization capability. Thousands of pages of literature formalized end-to-end by an AI swarm in 11 days points to a future where peer review and verification of active research get dramatically faster. Buzzard's own excitement is about what happens when machines start checking the Langlands program and flagging arguments that rely on things "known to the experts."

I'd discount one thing: this isn't the modern proof, and it doesn't produce a human-explorable document—two things Buzzard promised EPSRC. But as an autoformalization milestone, 11 days to FLT is genuinely impressive.

Source: Hacker News front page · xenaproject.wordpress.com
Published: Sep 5, 2026, 05:00 UTC+8 · 25 days ago