AI Signal 609 2 feeds carried it
Anthropic model formalizes Fermat's Last Theorem in Lean, completing Wiedijk's 100-challenge benchmark
↗
An Anthropic internal model used the prove2.me platform to produce a complete Lean formalization of Fermat's Last Theorem, generating over 13.4 million lines of code in an 11-day period and finishing the last item on Freek Wiedijk's 20-year-old list of 100 formalization challenges.
The formalization was produced by an AI model in 11 days rather than by years of human effort, demonstrating that large-scale autoformalization of complex mathematical literature is now feasible. For anyone building or relying on formal verification, this signals that automated tools may soon handle end-to-end formalization of hard material, though the resulting artifacts can be enormous and slow to compile, this proof takes nearly 20 times as long as Lean's entire mathematics library on a 96-core machine.
Written by elseif from the cluster below · every claim links back to a sourceThe three things worth knowing
Anthropic's internal model formalized a complete proof of Fermat's Last Theorem in Lean via the prove2.me platform, producing over 13.4 million lines of code in an 11-day period.
The proof uses the Darmon, Diamond, Taylor 1995 exposition rather than the modern proof, and completes Freek Wiedijk's list of 100 formalization challenges, a 20-year-old benchmark.
The author's EPSRC-funded project continues because it promises pull requests to Lean's mathlib and a human-exploitable dynamic document, neither of which Anthropic's work provides.
THE CLUSTER