A controversial proof in mathematics—one that has divided the field for over a decade—might finally be settled by an unlikely judge: a computer program. The heart of the debate revolves around Shinichi Mochizuki’s 2012 attempt to solve the ABC conjecture, a longstanding problem deeply rooted in the fundamental nature of numbers.
The ABC conjecture centers on a deceptively simple equation involving three whole numbers: a + b = c. It posits specific rules governing how prime numbers that make up these whole numbers must relate. Solving this seemingly basic problem could unlock profound insights into mathematics, potentially impacting other famous conjectures like Fermat’s Last Theorem.
Mochizuki, a professor at Kyoto University in Japan, presented his proof within a complex framework he invented called inter-universal Teichmüller (IUT) theory. However, the sheer technicality and obscurity of IUT theory rendered it largely incomprehensible to most mathematicians attempting to verify his work. Initial enthusiasm gave way to frustration as experts struggled to decipher its intricacies.
Adding fuel to the fire, in 2018, two prominent German mathematicians—Peter Scholze and Jakob Stix—identified a potential flaw within Mochizuki’s proof. Mochizuki countered their argument, and without an overarching body to arbitrate mathematical disputes, the field fractured into two camps: those largely accepting the mainstream view (supported by most mathematicians) and a smaller group aligned with Mochizuki and his institute in Kyoto.
Now, Mochizuki proposes a path forward through formalization—converting his proof from human-readable mathematical notation into Lean, a computer programming language specifically designed for rigorous mathematical verification. This process could potentially allow computers to automatically check the consistency of his arguments, offering an unprecedented level of objectivity.
Mochizuki believes Lean is uniquely equipped to navigate the complex linguistic and conceptual hurdles that have stalled progress in understanding IUT theory. He views it as a tool to liberate mathematical truth from the potential biases inherent in human interpretation.
While some experts like Kevin Buzzard at Imperial College London see this as a promising direction, they also acknowledge the monumental challenge ahead. Formalizing IUT theory would require translating vast swathes of intricate equations into Lean’s syntax—an undertaking akin to some of the largest formalization projects ever undertaken. Such efforts often involve dedicated teams of mathematicians and programmers spanning months or even years.
Johan Commelin from Utrecht University in the Netherlands, while cautiously optimistic, emphasizes that success hinges on Mochizuki’s sustained commitment. He cautions that if the project is abandoned prematurely, it might simply become another chapter in a protracted saga marked by unresolved disputes.
Even if successful, Commelin points out that even with computer-verified code, disagreements over interpretation could persist. Lean might resolve logical contradictions but not necessarily quell all philosophical or conceptual differences surrounding Mochizuki’s work.
Ultimately, while formalization offers a glimmer of hope for resolving this enduring mathematical standoff, it remains to be seen if it can overcome the deeply entrenched complexities and differing perspectives that have characterized the debate over the ABC conjecture proof.
