Andrew Wiles spent seven years in secret isolation, finally announcing his proof in 1993. It took two more years and a near-collapse to patch the gap. The proof, when published, ran 129 pages of dense mathematics that only a handful of people in the world could fully verify.
Now? AI is trying to formalize it.
Earlier this month, a workshop hosted at Imperial College London—funded by Logos Research and led by mathematician Kevin Buzzard—began using AI autoformalization tools to encode Wiles’s proof into machine-verifiable format. The twist: they didn’t pick an easy problem. They deliberately chose one of mathematics’ most complex proofs to test AI’s limits.
Fermat’s Last Theorem is simple to state: no three positive integers a, b, and c can satisfy the equation a^n + b^n = c^n for any integer value of n greater than 2. Pierre de Fermat claimed he had a “truly marvelous proof” that wouldn’t fit in the margin. He was probably wrong—the actual proof required mathematical machinery that didn’t exist for another 350 years.
The theorem itself isn’t what’s interesting here. What’s interesting is the process of formalization: translating human mathematical reasoning into a format that a computer can verify line by line, with zero tolerance for hand-waving.
This project sits at the intersection of two trends that have been accelerating through 2026.
First, AI reasoning is getting serious. We’re past the phase where AI could only regurgitate proofs it had seen in training data. The tools Buzzard’s team is using can attempt to bridge gaps, suggest formalization strategies, and catch subtle errors that humans miss.
Second, formal mathematics is having a moment. Lean, Coq, and other proof assistants have been around for years, but they’ve stayed niche—powerful tools used by a small priesthood. AI autoformalization could democratize access, turning these from specialist instruments into something working mathematicians actually use.
Nobody expects AI to find a new proof of Fermat’s Last Theorem. Wiles already did that. The question is whether AI can help us understand and verify what we already know with a rigor that human checking can’t match.
Machine verification doesn’t get tired. It doesn’t skip steps because they’re “obvious.” It doesn’t make sign errors at 2 AM. If Buzzard’s team succeeds—even partially—they’ll have built a map through territory that was previously only traversable by a few expert guides.
There’s something quietly profound about using machines to formalize one of humanity’s great intellectual achievements. Fermat wrote his note around 1637. Wiles completed the proof in 1995. And now, three decades later, we’re teaching software to read it.
The theorem is settled. But the story isn’t.
Sources: Imperial College London / Logos Research workshop (July 2026); Kevin Buzzard’s formalization research