This week's chart shows a proof tree. At its centre sits Fermat's Last Theorem, the 1637 conjecture that took Andrew Wiles seven years to crack, with the proof published in 1995. Around it branch 29,511 smaller theorems, each one a stepping stone Claude built and verified on the way to the root. Claude did this in 11 days, working largely on its own. It wrote 13 million lines of Lean code, more than five times the size of the entire community proof library it built upon.
Mathematics has always relied on peer review to catch errors, but that process can take years. Thomas Hales's proof of the Kepler conjecture sat under review for four years before twelve referees settled on "99% certain". If AI can formalise a proof this complex in under two weeks, that bottleneck starts to loosen. Errors get caught faster. Old results once taken on faith can finally be double-checked.
That benefit extends well beyond maths. Physics, engineering, and cryptography all lean on mathematical proofs they never fully re-verify themselves. Faster formal checking means fewer inherited mistakes sitting quietly in foundational work.
The limit is that checking is not the same as understanding. OpenAI's Astra model showed the other side of this coin in August, producing new results on ten unsolved problems, not just verifying old ones. Terence Tao, one of the world's leading mathematicians, warns that generation is now outpacing digestion and the slow human work of grasping why a proof is true.