Computers can verify mathematical proofs
monsitj/Getty Images
One of the most controversial debates in mathematics could be settled with the aid of a computer, potentially ending a bitter argument about a complex proof that has raged for more than a decade.
The trouble began in 2012, when Shinichi Mochizuki at Kyoto University in Japan stunned the mathematical world with a sprawling 500-page proof for the ABC conjecture, an important unsolved problem that strikes at the very heart of what numbers are. The proof used a highly technical and abstruse framework invented by Mochizuki, called inter-universal Teichmüller (IUT) theory, which appeared impenetrable even to most expert mathematicians seeking to understand it.
The ABC conjecture, which is now more than 40 years old, involves a seemingly simple equation of three whole integers, a + b = c, and dictates how the prime numbers that make up these numbers must relate to one another. As well as giving deep insights into the fundamental nature of how addition and multiplication interact, the conjecture has implications for other famous mathematical conjectures, such as Fermat’s Last Theorem.
These potential ramifications made mathematicians initially enthusiastic about verifying the proof, but early efforts faltered and Mochizuki bemoaned that more effort had not been made to digest the work. Then in 2018, two prominent German mathematicians, Peter Scholze at the University of Bonn and Jakob Stix at Goethe University Frankfurt, announced they had located a possible chink in the proof’s armour.
But Mochizuki rejected their argument and, with no grand adjudicating body to rule on who was right or wrong, the validity of IUT theory froze into two camps: on one side, most of the mathematical community; on the other, a small group of researchers loosely affiliated with Mochizuki and the Research Institute for Mathematical Sciences in Kyoto, where he is a professor.
Now, Mochizuki has proposed a possible solution to the stalemate. He has suggested translating the proof from its current form, in a mathematical notation designed for humans, to a programming language called Lean, which could be automatically checked and verified by a computer.
This process, called formalisation, is an ongoing area of research that could completely change the way mathematics is done. Formalising Mochizuki’s proof has been suggested before, but this is the first time he has indicated a desire to move forward with the project.
Mochizuki didn’t respond to a request for comment for this article, but in a recent report, he argued that Lean would be well suited to untangling the sorts of disagreements between mathematicians that have prevented the widespread acceptance of his proof: “[Lean] is the best and perhaps the only technology… for achieving meaningful progress with regard to the fundamental goal of liberating mathematical truth from the yoke of social and political dynamics,” writes Mochizuki.
According to Mochizuki, he was convinced of formalisation’s merits after attending a recent conference on Lean in Tokyo in July, in particular after seeing its ability to handle the sorts of mathematical structures he says are essential for his IUT theory.
This is a potentially promising direction for helping to break the impasse, says Kevin Buzzard at Imperial College London. “If it’s written down in Lean, then it’s not crazy, right? A lot of the stuff in the papers is written in a very strange language, but if you can write it down in Lean, then it means that at least this strange language has become a completely well-defined thing,” he says.
“We want to understand the why [of IUT], and we’ve been waiting for that for more than 10 years,” says Johan Commelin at Utrecht University in the Netherlands. “Lean would be able to help us understand those answers.”
However, both Buzzard and Commelin say that formalising IUT theory would be a mammoth undertaking and would involve translating reams of mathematical equations that currently only exist in human-readable form. This project would be on par with some of the largest formalisation efforts that have ever been completed, which often involve teams of expert mathematicians and Lean programmers, taking months or years.
This daunting prospect may be an unattractive proposition for the small handful of mathematicians qualified to take on the project. “People are going to have to make a big judgement call as to whether they want to sink a lot of their time into working on a project that ultimately might turn out to be a failure,” says Buzzard.
But even if mathematicians do manage to complete the project, and the Lean code shows that Mochizuki’s theorem has no contradictions, mathematicians including Mochizuki himself could still fight over its meaning, says Commelin.
“Lean can have a lot of impact and put an end to the controversy, but only if Mochizuki really sticks to his new resolution to formalise his work,” he says. “If he walks away after four months, saying, ‘Okay, I tried this, but Lean is just too stupid to understand my proof’, then it’s just a new chapter in a very long series of chapters where we’re still stuck with a social problem.”
And, for all the optimism that Mochizuki shows towards Lean, he also agrees with his critics that interpreting the code’s meaning could lead to further disagreements, writing that Lean “does not appear at the present time to constitute any of sort of “magical cure” for the complete resolution of social and political issues.”
However, Buzzard is hopeful that a successful formalisation might, at least, move the decade-long saga on, especially if Mochizuki succeeds. “You can’t argue with the software,” he says.
Topics:
