A decade-long dispute in mathematics over Shinichi Mochizuki's proof of the ABC conjecture may be resolved using computer formalization. Mochizuki has suggested translating his 500-page work into the Lean programming language for automated verification. This approach could bridge divides between conflicting camps in the mathematical community.
The controversy traces back to 2012, when Shinichi Mochizuki, a professor at Kyoto University in Japan, published a sprawling 500-page proof for the ABC conjecture. This 40-year-old problem concerns the equation a + b = c for whole integers and the relationships among their prime factors, with implications for theorems like Fermat’s Last Theorem. Mochizuki's proof relies on his intricate inter-universal Teichmüller (IUT) theory, which many experts found difficult to penetrate.
Initial enthusiasm waned as verification efforts stalled. In 2018, Peter Scholze from the University of Bonn and Jakob Stix from Goethe University Frankfurt identified a potential flaw, which Mochizuki disputed. Without a central authority, the math world split: most mathematicians on one side, and a smaller group affiliated with Mochizuki and Kyoto's Research Institute for Mathematical Sciences on the other.
To break the impasse, Mochizuki now advocates formalizing the proof in Lean, a language for computer-checked mathematics. Inspired by a July conference in Tokyo, he argues in a recent report that Lean could free mathematical truth from "social and political dynamics." As he writes, “[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.”
Experts see promise but caution. Kevin Buzzard of Imperial College London notes, “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.” Johan Commelin of Utrecht University adds, “We want to understand the why [of IUT], and we’ve been waiting for that for more than 10 years. Lean would be able to help us understand those answers.”
Yet, the task is immense, requiring teams of specialists and potentially years of work. Even success might not end debates over interpretation, as Mochizuki acknowledges Lean offers no "magical cure" for social issues. Buzzard remains optimistic: “You can’t argue with the software.”