AI Takes On Fermat's Last Theorem: Imperial College Feeds a Machine One of Math's Hardest Proofs — and the Result Is Refreshingly Honest

While everyone else burns cash on chips and AI that builds slide decks, a group of mathematicians in London did something unfashionable: they set AI loose on the proof of Fermat's Last Theorem.

Three key facts

From July 6 to 10, Imperial College London hosted a closed workshop on translating the proof of Fermat's Last Theorem into machine-checkable code. Led by mathematician Kevin Buzzard, the project uses the Lean theorem prover and aims to get the whole proof into Mathlib, the shared math library. It's funded by the UK's EPSRC through 2029 — just translating an already-proven theorem into a form a machine can verify takes years.

The workshop's backer is a tech company called Logos Research, and it wanted to test one thing: letting AI do the translating. The term of art is autoformalization — automatically rewriting a human-written proof into Lean code a machine can check line by line and find no gaps in. As AI gets stronger, they wanted to see which parts a machine can actually take over.

The honest answer: AI can only handle the scraps. The team's read is that the hard, definition-heavy, abstract pieces are likely beyond AI, while the parts where the definitions are already in Mathlib and the human literature spells everything out are where a machine might help. And they're not even formalizing Wiles's original 1994 proof — they're doing a more modern version.

WangDou's Take

This story has no billion-dollar valuation and no keynote, but it's more honest than most AI news. Silicon Valley shouts daily that AI is about to replace programmers and scientists — but drag it in front of Fermat's Last Theorem, one of the hardest proofs mathematicians know, and what it can actually do is the mover's job: copy out the passages where the definitions are already laid out and the humans have already written everything clearly. Anything that needs real thinking, a mathematician still has to do. That's the true water line of today's AI: a tireless, reasonably reliable copyist, nowhere near figuring out a proof on its own. A theorem proven thirty years ago will take until 2029 just to translate for a machine — which tells you how wildly the people promising original AI science next year are overselling. Real intelligence isn't measured by how flashy its slides are; it's whether it dares to stand in front of a problem like Fermat. Right now, it only dares to stand at the door and haul bricks.

Source: Xena / Kevin Buzzard · Imperial College FLT · Science News