Mathematicians plan computer proof of Fermat's last theorem

Mathematicians hope to develop a computerised proof of Fermat’s last theorem, an infamous statement about numbers that has beguiled them for centuries, in an ambitious, multi-year project that aims to demonstrate the potential of computer-assisted mathematical proofs.

Pierre de Fermat’s theorem, which he first proposed around 1640, states that there are no integers, or whole numbers, a, b, and c that satisfy the equation aⁿ + bⁿ = cⁿ for any integer n greater than 2. Fermat scribbled the claim in a book, famously writing: “I have discovered a truly marvellous proof of this, which this margin is too narrow to contain.”

It wasn’t until 1993 that Andrew Wiles, then at Princeton University, set the mathematical world alight by announcing he had a proof. Spanning more than 100 pages, the proof contained such advanced mathematics that it took more than two years for his colleagues to verify it didn’t contain any errors.

Many mathematicians hope that this work of checking, and eventually writing, proofs can be sped up by translating them into a computer-readable language. This process of formalisation would let computers instantly spot logical mistakes and, potentially, use the theorems as building blocks for other proofs.

But formalising modern proofs can itself be tricky and time-consuming, as much of the modern maths they rely on is yet to be made machine-readable. For this reason, formalising Fermat’s last theorem has long been considered far out of reach. “It was regarded as a tremendously ambitious proof just to prove it in the first place,” says Lawrence Paulson at the University of Cambridge.

Now, Kevin Buzzard at Imperial College London and his colleagues have announced plans to take on the challenge, attempting to formalise Fermat’s last theorem in a programming language called Lean.

“There’s no point in Fermat’s last theorem, it’s completely pointless. It doesn’t have any applications – either theoretical or practical – in the real world,” says Buzzard. “But it’s also a really hard question that’s become infamous because, for centuries, people have generated loads of brilliant new ideas in an attempt to solve it.”

He hopes that by formalising many of these ideas, which now include routine mathematical tools in number theory such as modular forms and Galois representations, it will help other researchers whose work is currently too far beyond the scope of computer assistants.

“It’s the kind of project that could have quite far-reaching and unexpected benefits and consequences,” says Chris Williams at the University of Nottingham, UK.

The proof itself will loosely follow Wiles’s, with slight modifications. A publicly available blueprint will be available online once the project is live, in April, so that anyone from Lean’s fast-growing community can contribute to formalising sections of the proof.

“Ten years ago, this would have taken an infinite amount of time,” says Buzzard. Even so, he will be concentrating on the project full-time from October, putting his teaching responsibilities on hold for five years in an effort to complete it.

“I think it’s unlikely he’ll be able to formalise the entire proof in the next five years, that would be a staggering achievement,” says Williams. “But because a lot of the tools that go into it are so ubiquitous now in number theory and arithmetic geometry, I’d expect any substantial progress towards it would be very useful in the future.”