A keenly debated proof in contemporary mathematics appears to be on the cusp of clarification. Two separate initiatives, both leveraging computer programs to shed new light on the existing controversy, are now actively underway. One of these projects has reportedly been operational in seclusion for over two years. These developments signal a potentially positive turning point, offering hope for a resolution to the long-standing mathematical disagreement, according to mathematicians familiar with the situation.
The dispute originated in 2012 when Shinichi Mochizuki, based at Kyoto University in Japan, published a 500-page document asserting a proof for a widely recognized mathematical concept known as the ABC conjecture. The conjecture itself is straightforward to articulate; it concerns the prime numbers that appear in solutions to the equation a + b = c and their interrelationships. However, a complete resolution of the conjecture necessitates profound comprehension of the intricate ways addition and multiplication interact. The implications of such a solution extend significantly across various branches of mathematics.
Mochizuki’s claimed proof was a notable event in the mathematical world. Its complexity and reliance on novel techniques and concepts, which he collectively termed Inter-universal Teichmüller (IUT) theory, posed considerable challenges for many of his peers. While prominent mathematicians dedicated months to dissecting Mochizuki’s work, engaging in discussions with him directly, the validation of the proof ultimately reached an impasse. The core issue was a difficulty in reaching a shared understanding of its validity.
A significant development occurred in 2018 when two respected mathematicians, Peter Scholze from the University of Bonn and Jakob Stix from Goethe University Frankfurt, both in Germany, indicated they had detected a potential flaw. Following their announcement, progress stalled. Mochizuki and a group of his close associates, predominantly from the Research Institute for Mathematical Sciences at Kyoto where he holds a professorship, maintained the stance that the proof was indeed correct. Conversely, a larger segment of the mathematical community held the view that the proof was either incomprehensible or, at best, fundamentally flawed.
Formalization as a Path Forward
Last year, Mochizuki extended an offer that could potentially bridge the gap between his perspective and that of his critics, proposing a direction for future progress. Substantial advancements had been made in a field known as formalization. This process involves meticulously translating written mathematical proofs into a computer-readable language, allowing for automated verification of their accuracy. Mochizuki expressed a particular affinity for a system named Lean, stating at the time that it represented the most suitable, and perhaps only, technology available for making genuine strides in the primary objective of divorcing mathematical truth from subjective social and political influences.
Currently, concerted efforts are underway to formalize Mochizuki’s proof of the ABC conjecture using the Lean system. At least two distinct groups of mathematicians have reported making progress. One of these groups is directly associated with Mochizuki himself, while the other has been working in secrecy for over two years. This latter group, however, has encountered its own obstacles.
The LANA Project and its Challenges
In late 2023, Katō Fumiharu, affiliated with the ZEN Mathematics Center in Japan, initiated the Lean and Anabelian geometry (LANA) project. This endeavor brought together mathematicians well-versed in Mochizuki’s work alongside specialists in Lean who had previously undertaken the formalization of other substantial mathematical undertakings. Adam Topaz of the University of Alberta, Canada, who was recruited by Fumiharu to assist with the formalization process, described the project’s main objective as simply “to settle the controversy once and for all.”
During a press conference held last month to announce the project, Fumiharu stated that the project’s members had achieved a “deep understanding” of Mochizuki’s theory in recent years. However, he also pointed to a specific area where progress was hindered, noting its close connection to the point that Scholze and Stix identified as problematic in 2018. “We’ve essentially gotten stuck in trying to understand a particular point in IUT,” Topaz explained. He further elaborated that this specific point had been isolated approximately eighteen months prior, with the initial expectation being that further study of the underlying theory would resolve the issue.
Despite extensive efforts, including participation in various workshops and indirect communication channels with Mochizuki via an intermediary, Topaz and his collaborators were unable to advance beyond this particular challenge.
Mochizuki’s Perspective and the Lean Formalization Initiative
In parallel, Mochizuki and his colleagues have also launched their own project to formalize the theorem using Lean. Their primary motivation differs from that of the LANA project; rather than focusing on proving correctness, Mochizuki maintains that the proof is already established. For him, the value of this undertaking lies more within the realm of communication. He articulated at a recent conference at the University of Exeter, UK, that “This verification aspect is not a central focal point of interest.” Instead, he posits, “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’s team is concentrating its efforts on the contentious segment of the proof that proved problematic for the LANA project and was first highlighted by Scholze and Stix. Their plan is to subsequently formalize a foundational framework comprising four additional stages. Mochizuki claims they have made initial progress by generating about 70 lines of Lean code, though this material is not yet publicly accessible.
Kevin Buzzard of Imperial College London expressed skepticism regarding the completeness of this initial code, noting, “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.”
Despite these reservations, this represents some of the most substantial and promising progress in understanding Mochizuki’s proof since its initial publication. “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,” Buzzard remarked.
Topaz echoes this sentiment, acknowledging the inherent difficulties but identifying a potential path forward, particularly given Mochizuki’s open engagement with the LANA project, despite their distinct operational approaches. “Now that there’s this dialogue with Mochizuki using Lean, I’m actually quite optimistic that there could be a resolution to this controversy,” Topaz stated. “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.”