Mathematicians Put AI to Work Formalizing Fermat's Last Theorem

At a workshop hosted by Imperial College London this month, mathematicians turned artificial intelligence loose on one of the most storied problems in their field — not to prove Fermat's Last Theorem, which Andrew Wiles famously did in the 1990s, but to translate its sprawling modern proof into code a computer can verify line by line.

The Project

The effort is part of an EPSRC-funded project led by Professor Kevin Buzzard to formalize Fermat's Last Theorem in Lean, the proof assistant that has become the mathematical community's tool of choice for machine-checkable proofs. The formalization aims to encode a "21st century" version of the proof, incorporating later developments by Khare–Wintenberger, Kisin, and others — a body of mathematics so vast that formalizing it by hand is a multi-year, many-person undertaking.

To date, roughly 30 people have contributed code to the project, with just over 60 contributions verified and accepted. It is precisely the kind of long, technical slog where the workshop's organizers saw an opening for AI.

AI Enters the Proof

With autoformalization — the automated translation of ordinary mathematical prose into formal Lean code — growing more capable, the research firm Logos Research proposed experimenting with having AI formalize the many prerequisite lemmas the proof depends on, and perhaps eventually main proof ideas themselves.

The appeal is straightforward. Formalizing a major theorem requires encoding thousands of supporting results, definitions, and technical lemmas, most of them individually unremarkable but collectively enormous. If AI can reliably formalize this scaffolding, human mathematicians can focus their effort on the genuinely hard conceptual steps — a division of labor that could dramatically accelerate the entire enterprise of formal mathematics.

Why It Matters Beyond Fermat

The Fermat project is a proving ground for a broader shift. As AI systems grow more capable at mathematical reasoning, the question of how to trust their output becomes central — and formal verification offers an answer: a proof that type-checks in Lean is correct, whatever produced it. Marrying AI's generative speed with Lean's rigorous checking could yield a new mode of mathematical work, where machines propose and formal systems dispose.

There's a data flywheel, too. The formalized proofs these projects produce become high-quality training material for the next generation of mathematical AI — the same virtuous loop visible in Mistral's newly released Leanstral 1.5, which saturates formal-math benchmarks and now finds real bugs in software. Each formalized theorem makes the models a little better at formalizing the next.

Whether AI meaningfully accelerates the Fermat formalization remains to be seen; the workshop was an experiment, not a triumph. But the symbolism is hard to miss. The theorem that took mathematicians 350 years to prove, and Wiles the better part of a decade to crack, is now a testbed for whether machines can help carry mathematics' heaviest loads.