Computers can check mathematical proofs
monsitj/Getty Images
One of the most controversial debates in mathematics could be resolved using a computer, potentially ending a bitter dispute over a complex proof that has raged for more than a decade.
The problems started in 2012 when Shinichi Mochizuki at Kyoto University in Japan stunned the mathematical world with an extensive 500-page proof of the ABC Conjecture, an important unsolved problem that goes to the very core of what numbers are. The proof used a highly technical and intricate structure invented by Mochizuki called Interuniversal Teichmüller Theory (IUT), which seemed incomprehensible even to most experienced mathematicians seeking to understand it.
The ABC hypothesis, now over 40 years old, involves the seemingly simple equation of three integers, a + b = c, and specifies how the primes that make up those numbers should relate to each other. This conjecture not only provides deep insight into the fundamental nature of the interaction between addition and multiplication, but also has implications for other well-known mathematical conjectures such as Fermat's Last Theorem.
These potential implications initially made mathematicians enthusiastic about testing the proof, but early attempts failed and Mochizuki lamented that more effort had not been made to digest the work. Then in 2018 two outstanding German mathematicians Peter Scholze at the University of Bonn and Jacob Stix at the Goethe University in Frankfurt announced that they have discovered a possible chink in the armor of evidence.
But Mochizuki rejected their arguments, and in the absence of any high judiciary body that could decide who was right and who was wrong, the validity of the IUT theory froze in two camps: on the one hand, most of the mathematical community; on the other hand, a small group of researchers loosely associated with Mochizuki and the Mathematical Sciences Research Institute in Kyoto, where he is a professor.
Now Mochizuki has proposed a possible way out of the impasse. He proposed translating the proof from its current form in mathematical notation intended for humans into a programming language called Lean that could be automatically checked and verified by a computer.
This process, called formalization, is an ongoing area of research that can completely change the way we learn math. It had been proposed to formalize Mochizuki's proof before, but this was the first time he expressed a desire to continue working on the project.
Mochizuki did not respond to requests for comment for this article, but recent reporthe argued that Lin was well suited to untangling the disagreements among mathematicians that prevented his proof from being widely accepted: “[Lean] “is the best and perhaps the only technology… for making meaningful progress towards the fundamental goal of liberating mathematical truth from the yoke of social and political dynamics,” writes Mochizuki.
Mochizuki says he became convinced of the merits of formalization after attending a recent lean manufacturing conference in Tokyo in July, particularly after seeing its ability to handle the kinds of mathematical structures he says are necessary for his IUT theory.
This is a potentially promising direction that will help break the impasse, says Kevin Buzzard at Imperial College London. “If it's written in Lean, it's not crazy, is it? A lot of things in newspapers are written in very strange language, but if you can write it in Lean, then that means at least that strange language has become a very well-defined thing,” he says.
“We want to understand why [of IUT]and we have been waiting for this for more than 10 years,” says Johan Commelin at Utrecht University in the Netherlands. “Lean can help us understand these answers.”
However, both Buzzard and Commelin say formalizing IUT theory will be a mammoth task and require translating many mathematical equations that currently exist only in human-readable form. This project would rival some of the largest formalization efforts ever undertaken, often involving teams of experienced mathematicians and lean programmers over months or years.
This daunting prospect may not be attractive to the small handful of mathematicians capable of taking on the project. “People are going to have to make a big decision about whether they want to spend a lot of time working on a project that could end up being a failure,” says Buzzard.
But even if the mathematicians succeed in completing the project and the Lean code shows that Mochizuki's theorem is consistent, mathematicians, including Mochizuki himself, may still argue about its meaning, Commelin says.
“Lean can have a big impact and end the controversy, but only if Mochizuki really sticks to his new decision to formalize his work,” he says. “If he leaves four months later saying, 'OK, I tried it, but Lin is too stupid to understand my proof,' then it's just a new chapter in a very long series of chapters in which we're still stuck with a social problem.”
And for all the optimism Mochizuki expresses about lean, he also agrees with his critics that interpretation of the code's meaning could lead to further disagreement, writing that lean “does not currently represent a kind of 'magic cure' for completely solving social and political problems.”
Still, Buzzard is hopeful that a successful formalization could at least move the decade-long saga forward, especially if Mochizuki is successful. “You can't argue with software,” he says.
Topics:
