science
Mathematicians Launch Lean Formalization Efforts for Disputed ABC Conjecture Proof
Two separate efforts are underway to formalize Shinichi Mochizuki's controversial proof of the ABC conjecture in Lean, including a secretive project that has hit a roadblock. The initiatives aim to resolve a long-standing debate in number theory. @NewScientist reported on the developments involving mathematicians from Japan, Germany, Canada, and the UK.
Apr 21, 9:58 AM·2m read4 sources
NE
+1
newscientist.comAudio version
Tap play to generate a narrated version.
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.
