Mathematicians plan computer proof of Fermat’s last theorem
Fermat’s last theorem puzzled mathematicians for centuries until it was finally proven in 1993. Now, researchers want to create a version of the proof that can be formally checked by a computer for any errors in logic
By Alex Wilkins
18 March 2024
Pierre de Fermat’s scribblings set mathematicians on a centuries-long quest
GRANGER Historical Picture Archive/Alamy
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 an + bn = cn 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.”
Read more
Mathematicians found a guaranteed way to win the lottery in 2023
Advertisement
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.
