“I have found a really admirable demonstration, but the margin of the book is very small to put it.” It is what the 17th -century French mathematician Pierre de Fermat wrote when stating his His “last theorem”. Fermat’s problem took three decades to be found between the mathematician papers and three centuries until that admirable test was discovered.
And yet the case is not entirely settled, only that the challenge is something different.
Take it to a computer. He New challenge It is to make a computer to try the elusive theorem. That is the objective of a new project, FERMAT FORMALISINGled by Imperial College London.
Fermat’s problem. Fermat’s last theorem “postulates that, if A, byc are natural numbers and not equal to zero, the an+bn = cn equation has no solution if n is greater than two. Formally demonstrating something is not as simple as trying it by rehearsal and error, and this demonstration, too complex for the “megish margin” of the Fermat’s notebook would be lost for centuries.
The problem was resolved in 1994 by the British Andrew Wiles, who had begun to solve this puzzle with only 10 years. In 2016 Wiles was awarded the ABEL award, the award considered “The Nobel of Mathematics.”
Almost one million pounds. Another 30 years after the resolution of the enigma and more than three centuries after the death of Fermat, a team of researchers, led by Kevin Buzzard, of Imperial College London, has put to work to take a different step, teach A computer to solve this problem.
The new project It began at the end of 2024 and will last until 2029. It has a financing of just over 934,000 pounds and already begins to give some results, in the form of code fragments that are added to a Database in Github.
What remains to be resolved.It can be contraintuitive, but this type of reasoning, which lead us to formally demonstrate mathematical theorems, are difficult to teach computers.
Recently, Buzzard and other experts They explained the complexity of the matter to the French newspaper I monde. To begin with, we must take into account that the resolution of this theorem is complex, it is no accident that several generations of mathematics would turn the brains trying to find it.
These mathematicians also had previous experience in the field of resolution of these types of problems. As Buzzard explained to the French newspaper, mathematicians have a base that allows them to “jump steps” when explaining the resolution to this problem. A computer, however, must start from scratch when building its own explanation for the matter.
And all this, for what? “Fermat’s last theorem (…) has no applications, theoretical or practices, in the real world,” Buzzard pointed out A few months ago to the magazine New Scientist. So why so much effort to teach a computer to solve something we already resolved? The key here is not in the past but in the future.
According to Explain the team at the head of the projectcomputers today can be used to attend mathematicians trying to solve problems such as demonstration of theorems, but there is an obstacle to materializing some forms of help.
The problem, they point out, is that few mathematicians have focused on working with this software, so there are no tools that have the “definitions” used by mathematicians to solve these problems. Working on this problem should be used to create the necessary databases for solving similar problems in the future.
In Xataka | We had more than a century trying to solve some mathematical problems. The AI is starting to unravel
Image | Diofanto’s arithmetic / Pierre de Fermat by Rolland Lefebvre
