In 2012, Shinichi Mochizuki published a paper that claimed to provide a proof for the ABC conjecture in number theory
Newscom/Alamy
One of the most hotly contested proofs in modern mathematics may be on the verge of unraveling. Two projects, both aimed at using a computer program to shed new light on the dispute, are now up and running – one of which has been operating in secret for more than two years. The development is a positive sign that the series might find a solution, mathematicians say.
The saga began in 2012 when Shinichi Mochizuki at Kyoto University in Japan claimed to have proved a famous idea called the ABC Conjecture and published a 500-page proof online. The conjecture is simple to state, concerning the prime numbers involved in the solution of the equation a + b = ca of how these numbers are related. But solving it requires deep insight into the nature of how addition and multiplication interact. The answer also has far-reaching implications for other mathematical disciplines.
Mochizuki’s proof was a mathematical bombshell, but difficult for many of his colleagues to understand because it contained new techniques and concepts that he collectively called the Inter-universal Teichmüller theory (IUT). Prominent mathematicians spent the following months trying to clarify Mochizuki’s work, including interviews with Mochizuki himself, but the correctness of the proof reached an impasse.
In 2018, after two prominent mathematicians – Petr Scholz at the University of Bonn and Jakob Stix at Goethe University Frankfurt, both in Germany – announced that they had identified a possible bug, no further progress was made. Mochizuki and a cadre of close colleagues, mostly at Kyoto University, argued that the proof was correct, while much of the mathematical community argued that the proof was at best indecipherable and at worst fatally flawed.
Last year, however, Mochizuki offered his detractors an olive branch and a potential way forward. Huge progress has been made in an area of mathematics called formalization, where written mathematical proofs are translated into a computer language that can automatically verify their correctness. One particular language, called Lean, appealed to Mochizuki the most. He then wrote that: “[Lean] is the best and perhaps the only technology… for making meaningful progress with respect to the fundamental goal of liberating mathematical truth from the yoke of social and political dynamics.
Efforts are now officially underway to formalize Mochizuki’s proof of the ABC conjecture in Lean, with at least two separate mathematical groups reporting progress, including one run by Mochizuki and another that has been operating in secret for more than two years but has hit a roadblock.
By the end of 2023, Kato Fumiharu at the ZEN Mathematics Center in Japan he started the Lean and Anabelian geometry (LANA) project involving mathematicians who were familiar with Mochizuki’s work as well as Lean experts who formalized other major mathematical projects. The primary goal was “just to settle the dispute once and for all,” he says Adam Topaz at the University of Alberta in Canada, whom Fumiharu recruited to help formalize the proof.
At the press conference last month announcing the project, Fumiharu said that members had “deeply understood” Mochizuki’s idea over the past few years, but there was also a specific point where they couldn’t make progress, closely related to the area Scholze and Stix identified as containing a possible flaw in 2018. “Basically, we’re stuck trying to understand a specific point in IUT,” says Topaz. “We isolated this point almost a year and a half ago and originally thought we needed to understand more theory to be able to overcome this potential problem.”
But even after Fumiharu and his colleagues tried to understand it through various workshops and indirect communication with Mochizuki through an intermediary, they could not make any progress.
In a separate development, Mochizuki and his colleagues also started a project to formalize the proof using Lean. However, they are less interested in proving it correct, as Mochizuki claims it is already correct. Instead, they see the value of the project more in communication.
“This verification aspect is not a central concern,” Mochizuki said at a recent conference at the University of Exeter in the UK. “The importance of Lean formalization is to create a precise record of the logical structure of the IUT that is immune to spurious misinterpretations and can therefore be used to communicate this simplicity in the most efficient and accurate way to other mathematicians.”
Mochizuki and his team’s approach is to focus on a controversial area of evidence where the LANA project has stalled, which Scholze and Stix first identified before moving on to formalize a plan with four additional phases. Mochizuki says they started doing this by creating 70 lines of Lean code to start with, though it’s not yet publicly available.
This isn’t a lot of code, he says Kevin Buzzard at Imperial College London. “It’s going to be a lot more than 70 lines. At 70 lines, you’re trying to prove a couple of college-level theorems, let alone a gigantic proof.”
However, this is still one of the most promising and significant advances in understanding Mochizuki’s proof since it was first announced. “There’s been no movement, no interesting new information that’s at all relevant, and this is the first time you feel like maybe things are actually moving,” Buzzard says.
Topaz agrees that despite the difficulties, there still seems to be a possible way forward, especially since Mochizuki has openly communicated with the LANA project, even as the groups’ efforts remain divergent.
“Now that this dialogue is going on with Mochizuki using Lean, I’m actually quite optimistic that this controversy could be resolved,” says Topaz. “If there’s one thing that gives me the most optimism right now, it’s that we’re having this back-and-forth dialogue with the Mochizuki group.
topics:
Leave a Reply