Adapted by:
Pablo Martínez-Juarez
WriterEnvironmental economist and science journalist. For a few years, I worked as a researcher on the economics of climate change adaptation. Now I write about that and much more.
Alba Mora
WriterAn established tech journalist, I entered the world of consumer tech by chance in 2018. In my writing and translating career, I've also covered a diverse range of topics, including entertainment, travel, science, and the economy.
When the 17th-century French mathematician Pierre de Fermat announced his last theorem, he wrote in a copy of Diophantus’ Arithmetica, “I have discovered a truly remarkable proof which this margin is too small to contain.” Years later, his son found the marginal note among his papers. In the 1990s, an English mathematician finally proved Fremat’s last theorem.
Proving the theorem again. However, the case isn’t entirely settled. The challenge has simply changed. A new project led by Imperial College London, Formalising Fermat, aims to prove the theorem using a computer.
Fermat’s last theorem. Fermat’s last theorem states that if a, b, and care natural numbers and not equal to zero, the equation a^n + b^n = c^n has no solution if n is greater than 2. Formally proving something isn’t as simple as verifying it through trial and error. Additionally, this proof–too complex for the meager margin of Diophantus’ Arithmetica–would remain lost for centuries.
British mathematician Andrew Wiles, who first learned about Fermat’s last theorem at age 10, finally solved it in 1994. In 2016, Wiles was awarded the Abel Prize, which is considered the “Nobel Prize of mathematics.”
A million dollars. 30 years after Wiles solved the enigma and more than three centuries after Fermat’s death, researchers have embarked on a new project. The team at Imperial College London aims to teach a computer to solve the last theorem.
The project, which was funded by nearly $1.2 million, began in late 2024 and will run until 2029. It’s already started yielding results, including code snippets that researchers add to a database on GitHub.
What remains to be solved. Ironically, the kind of reasoning that allows scientists to prove mathematical theorems formally is difficult to teach computers.
Project leader Kevin Buzzard and other experts recently discussed the intricacies of this issue with the French newspaper Le Monde. First, it’s important to recognize that solving Fermat’s last theorem is no small feat. Several generations of mathematicians struggled to find a solution.
Additionally, these mathematicians often had prior experience in tackling similar problems. As such, they possessed a foundation that allowed them to “skip steps” when articulating their solutions. In contrast, a computer must start from scratch when constructing its own explanation for the problem.
What for? “There’s no point in Fermat’s last theorem... It doesn’t have any applications–either theoretical or practical–in the real world,” Buzzard told New Scientist in 2024. So, why invest so much effort into teaching a computer to solve a problem that mathematicians have already resolved? The answer lies not in the past but in the future.
The Imperial College London team explains that computers today can assist mathematicians in solving problems, like proving theorems. However, there’s a big barrier to making this assistance effective.
According to researchers, this barrier stems from the fact that few mathematicians have used this software, resulting in a lack of tools containing the “definitions” used to address these issues. By tackling this problem, the goal is to create the necessary databases that can be used to solve similar problems in the future.
Images | Clayton Robbins | Diaphontus’ Arithmetica | Portrait of Pierre de Fermat by Rolland Lefebvre
Log in to leave a comment