Mathematicians Launch Lean Formalization Efforts for Disputed ABC Conjecture Proof

Two groups of mathematicians have initiated projects to formalize Shinichi Mochizuki's disputed proof of the ABC conjecture using the Lean programming language, with one effort underway for over two years and currently addressing a specific challenge in the theory.

In a press conference last month, Kato Fumiharu announced that members of the Lean and Anabelian geometry (LANA) project had developed a deep understanding of Mochizuki’s ideas over the past few years. The project, started late in 2023 at the ZEN Mathematics Center in Japan, enlisted mathematicians familiar with Mochizuki’s work and Lean experts.

Fumiharu said the team identified a specific point they couldn’t progress on, related to an area previously flagged as potentially erroneous. Adam Topaz at the University of Alberta, Canada, stated that the primary goal of the LANA project was to settle the controversy once and for all.

Topaz added that the team had gotten stuck in trying to understand a particular point in Inter-universal Teichmüller theory (IUT), isolating this issue almost a year and a half ago.

@NewScientist reported that the sticking point aligns with concerns raised in 2018 by Peter Scholze at the University of Bonn, Germany, and Jakob Stix at Goethe University Frankfurt, Germany, who announced they had identified a possible error in Mochizuki’s proof.

Separately, Mochizuki and his colleagues have started their own project to formalize the proof using Lean. Mochizuki told a recent conference at the University of Exeter, UK, that this verification aspect is not a central focal point of interest.

He stated that 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 produced 70 lines of Lean code as a start for formalizing the controversial area of the proof. Kevin Buzzard at Imperial College London stated that it’s going to be a lot more than 70 lines to formalize the proof.

@NewScientist reported that Mochizuki’s group is focusing on the disputed section before expanding to a blueprint with four further stages. The controversy originated in 2012 when Mochizuki at Kyoto University, Japan, published a 500-page paper claiming to prove the ABC conjecture in number theory. The ABC conjecture concerns prime numbers involved in solutions to the equation a + b = c.

Mochizuki’s proof features new techniques and concepts called Inter-universal Teichmüller theory (IUT). Last year, Mochizuki offered to use the Lean formalization language for his proof. He stated 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.

@NewScientist reported that these developments represent some of the most promising progress since the proof's initial announcement, with potential for dialogue between the groups to resolve the impasse.