Mathematicians put AI to work on Fermat's Last Theorem

What happened

Mathematicians including Kevin Buzzard of Imperial College London launched a workshop to encode a formal proof of Fermat's Last Theorem into the Lean proof assistant library Mathlib, with significant AI tool assistance.

Context and impact

Fermat's Last Theorem was proved by Andrew Wiles in 1993, but the proof has never been formally machine-verified. The project is both symbolic and practical: AI is becoming an accelerator for formal mathematics. It raises a philosophical question — if a machine verifies a proof humans cannot fully grasp, what have we truly achieved?

Details

• Project lead: Kevin Buzzard, Imperial College London
• Goal: encode Fermat's Last Theorem into Mathlib (Lean proof assistant)
• Day-one result: codebase grew from 20,000 to 40,000 lines
• AI role: assist with writing formal proofs and refactoring code
• Workshop: united mathematicians, computer scientists, and AI specialists in London