Anthropic formalized Fermat’s Last Theorem with Claude writing thirteen million lines of Lean in eleven days. The part worth sitting with is that Lean can check every link in a chain that took humans years to trust the first time around.

Wiles’s 1995 proof needed months of review before a gap showed up, then another year to close it. That verification tax is what AI-generated math is about to dump on the community at scale, and machine-checked formalization is one of the few ways the load stays manageable.

So the useful question is whether we can grade model-written proofs without burning years of referee time.

https://www.anthropic.com/research/formalizing-fermats-last-theorem