One of the most highly debated proofs in contemporary mathematics may soon find resolution. Two innovative projects are underway, utilizing computer programs to illuminate this ongoing controversy—one of which has operated in secrecy for over two years. Mathematicians express optimism about these developments as they could lead to a breakthrough in this heated debate.

This narrative traces back to 2012 when Shinichi Mochizuki, a professor at Kyoto University in Japan, proclaimed that he had demonstrated a significant concept known as the ABC conjecture, releasing a staggering 500-page document online. This conjecture is simply stated concerning prime numbers in the equation a + b = c and their interrelations. However, solving it necessitates profound insights into the interplay of addition and multiplication, and its ramifications extend deeply into various mathematical realms.

Mochizuki’s proof was explosive but regarded as esoteric by many colleagues due to its innovative techniques and concepts collectively referred to as interuniversal Teichmüller theory (IUT). A slew of prominent mathematicians engaged for months in efforts to distill Mochizuki’s work, including discussions with him, ultimately hitting a standstill regarding the proof’s correctness.

In 2018, two notable mathematicians—Peter Scholze from the University of Bonn and Jacob Stix from Goethe University Frankfurt—claimed they had found a potential flaw. Despite this, no further progress was achieved. While Mochizuki and his close associates at Kyoto University maintained that the proof was valid, the broader mathematical community viewed it as either incomprehensible or fundamentally flawed.

However, last year, Mochizuki reached out to his critics, proposing a possible way forward. Notable advancements in a field called formalization have emerged, allowing mathematical proofs to be transcribed into computer language for automatic correctness verification. A specific language known as Lean captured Mochizuki’s interest. He remarked at the time: “[Lean] is perhaps the best and only technology to advance the goal of liberating mathematical truth from the constraints of social and political dynamics.”

Currently, efforts to formalize Mochizuki’s ABC conjecture proof in Lean are underway, with multiple mathematical groups announcing significant progress. This includes Mochizuki’s team and another group that has been progressing in secret for over two years but has encountered challenges.

In late 2023, Bunji Kato from Japan’s ZEN Mathematics Center, initiated the Lean Geometry and Annabelle Geometry (LANA) project, uniting mathematicians familiar with Mochizuki’s work and Lean experts who have crystallized other complex mathematical endeavors. The primary aim is to “finally resolve the dispute,” as stated by Kato. They enlisted Adam Topaz from the University of Alberta to facilitate the formalization of the proof.

During a press conference held last month to announce the project, Kato indicated that through the years, team members have developed a “deeper understanding” of Mochizuki’s ideas. Nevertheless, they faced hurdles specifically tied to issues flagged by Scholze and Stix in 2018. Topaz commented, “We essentially stalled while attempting to assimilate certain aspects of IUT. We recognized this issue about a year and a half ago, initially believing a better understanding of the theory would avert this potential complication.”

Despite numerous workshops and indirect communications with Mochizuki, the team has struggled to move forward.

In a parallel initiative, Mochizuki and his associates have also begun to formalize proofs utilizing Lean. Their goal, however, is not to confirm Mochizuki’s position, as he already asserts its correctness, but emphasizes the project’s value in enhancing communication.

Mochizuki stated at a recent conference at the University of Exeter, “The validation aspect is not our primary focus. The significance of Lean formalization lies in establishing an accurate record of the logical structure of IUT, free from misinterpretations, ensuring it can effectively communicate its essence to other mathematicians.”

Mochizuki and his team’s strategy involves focusing on the contentious areas of evidence previously identified by Scholze and Stix, where the LANA initiative has stagnated. They aim to create a formal blueprint that encompasses four additional steps. Mochizuki has commenced this process by drafting 70 lines of Lean code, though it has not yet been made public.

This code, according to Kevin Buzzard of Imperial College London, is minimal. “Seventy lines hardly suffice; you would struggle to prove even a few undergraduate-level theorems within that.”

However, these developments are among the most promising advancements in comprehending Mochizuki’s proof since its debut. “We haven’t seen much movement, no new relevant information, and this is the first time I sense actual momentum,” Buzzard observes.

Topaz shares that despite existing challenges, he remains hopeful for progress, although the group’s precise efforts remain uncertain, especially as Mochizuki maintains communication with the LANA project.

“I’m quite optimistic that we might find a resolution to this controversy due to the dialogues I’ve had with Mr. Mochizuki regarding Lean,” Topaz adds. “What excites me the most is that we are engaging in reciprocal discussions with Mr. Mochizuki’s team.”