ABC conjecture: The secret project to settle controversial maths proof with a computer

One of the most bitterly contested proofs in modern mathematics may be on the verge of being untangled. Two projects, both aiming to use a computer program to cast new light on the controversy, are now up and running – with one having operated in secret for more than two years already. The developments are a positive sign that the row might find a solution, say mathematicians.

The saga began in 2012 when Shinichi Mochizuki at Kyoto University, Japan, claimed to have proved a famous idea called the ABC conjecture, posting a 500-page proof online. The conjecture is simple to state, concerning prime numbers involved in solutions to the equation a + b = c and how these numbers relate to each other. But solving it requires deep insights 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 it was difficult for many of his colleagues to understand because it featured new techniques and concepts, which he collectively called Inter-universal Teichmüller theory (IUT). Prominent mathematicians spent the following months trying to clarify Mochizuki’s work, including in conversations with Mochizuki himself, but the correctness of the proof reached an impasse.

In 2018, after two prominent mathematicians – Peter Scholze at the University of Bonn and Jakob Stix at Goethe University Frankfurt, both in Germany – announced they had identified a possible error, there was no further progress. Mochizuki and a cadre of close colleagues, mostly at Kyoto University, maintained the proof was correct, while a larger part of the mathematical community argued that the proof was at best indecipherable and at worst fatally flawed.

Last year, however, Mochizuki offered an olive branch to his naysayers and a potential path forward. There had been immense progress in an area of mathematics called formalisation, where written mathematical proofs are translated to a computer language that can verify their correctness automatically. One particular language, called Lean, appealed to Mochizuki the most. He wrote at the time that: “[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.”

Now, efforts to formalise Mochizuki’s proof of the ABC conjecture in Lean are officially under way, with at least two separate mathematical groups announcing progress, including one helmed by Mochizuki and another that has been operating in secret for more than two years, but has hit a roadblock.

Late in 2023, Kato Fumiharu at the ZEN Mathematics Center in Japan started the Lean and Anabelian geometry (LANA) project, enlisting mathematicians who were familiar with Mochizuki’s work as well as experts in Lean who had formalised other large mathematical projects. The primary goal was “just to settle the controversy once and for all”, says Adam Topaz at the University of Alberta, Canada, who Fumiharu recruited to help with formalising the proof.

In a press conference last month announcing the project, Fumiharu said members had come to a “deep understanding” of Mochizuki’s idea over the past few years, but there was also a specific point they couldn’t progress on, which is closely related to the area that Scholze and Stix identified as containing a possible error in 2018. “We’ve essentially gotten stuck in trying to understand a particular point in IUT,” says Topaz. “We isolated this point almost a year and a half ago now, and originally we thought we just needed to understand more of the theory to be able to get past this potential issue.”

But even after trying to understand it through various workshops and indirect communication with Mochizuki via an intermediary, Fumiharu and his colleagues couldn’t make progress.

In a separate development, Mochizuki and his colleagues have also started a project to formalise the proof using Lean. But they are less interested in proving its correctness, as Mochizuki maintains it is already correct. Instead, he sees the value of the project more in communication.

“This verification aspect is not a central focal point of interest,” Mochizuki told a recent conference at the University of Exeter, UK. “The significance of Lean formalisation lies in producing a precise record of the logical structure of IUT that is immune to false misinterpretations, and hence can be used to communicate this simplicity in a maximally efficient or precise way to other mathematicians.”

Mochizuki and his team’s approach is to focus on the controversial area of the proof that the LANA project became stuck on, and that Scholze and Stix first identified, before moving on to formalising a blueprint with four further stages. Mochizuki claims they have begun to do this by producing 70 lines of Lean code as a start, though it isn’t yet publicly available.

This isn’t much code, says Kevin Buzzard at Imperial College London. “It’s going to be a lot more than 70 lines. At 70 lines, you’re struggling to prove a couple of undergraduate-level theorems, let alone a gigantic proof.”

However, it is still some of the most promising and significant progress in understanding Mochizuki’s proof since it was first announced. “There’s been no movement, no interesting new information of any relevance at all, and this is the first time that you feel that maybe things are actually moving,” says Buzzard.

Topaz agrees that, despite the difficulties, there still looks to be a possible way forward, especially as Mochizuki was openly communicating with the LANA project, even though the groups’ efforts remained distinct.

“Now that there’s this dialogue with Mochizuki using Lean, I’m actually quite optimistic that there could be a resolution to this controversy,” says Topaz. “If anything gives me the most optimism at this point, it’s that we have this dialogue going back and forth with Mochizuki’s group.”