Mathematicians still can’t settle the ABC conjecture controversy

In 2012 Shinichi Mochizuki, a professor at Kyoto University, shocked the mathematical world by posting a 500‑page argument claiming to finally prove the ABC conjecture – a deceptively simple statement about the relationship between the prime factors of three integers that satisfy a + b = c. For decades the conjecture had resisted attack, so the announcement sparked a mixture of awe and skepticism.

The controversy didn’t stem from the result itself; it was the machinery behind it. Mochizuki built an entirely new edifice of mathematics called Inter‑universal Teichmüller (IUT) theory. No one had ever seen anything like it, and only a handful of specialists felt comfortable navigating its labyrinthine pages. Consequently, while a small cohort announced belief in the proof, a larger community remained unconvinced, citing gaps they could not locate or understand.

Enter the idea of computer‑assisted verification. If a proof can be encoded in a formal language – for example, the Lean proof assistant – a computer can mechanically check every inference, leaving no room for human misinterpretation. Two groups set out to do exactly that. One was led by Mochizuki himself, and the other, based at the ZEN Mathematics Center in Japan, became known as the LANA (Lean and Anabelian Geometry) project.

Last month LANA released an interim report that, rather than presenting a finished formalisation, laid bare the obstacles it has encountered. The authors describe “lively discussions” among the five core members, yet admit they have not reached a consensus on whether IUT theory even survives a formal check.

At the heart of the difficulty lies what the report calls “the wall”. This refers to a flaw identified in 2018 by two leading mathematicians, Peter Scholze (University of Bonn) and Jakob Stix (Goethe University Frankfurt). Their criticism exposed a subtle inconsistency in the IUT framework that, according to the LANA authors, still haunts any attempt to translate the argument into Lean code.

When New Scientist reached out to the five LANA participants for comment, none responded at the time of writing. Meanwhile, senior voices outside the project are speaking up. Abhishek Saha of Queen Mary University of London notes that most of his colleagues view IUT as “seriously flawed”, and the lack of progress on formalisation seems to confirm that intuition.

Chris Bowman‑Scargill from the University of York adds a practical concern: a substantial body of subsequent research has been built on the presumed validity of IUT. If the foundation collapses, a cascade of results could be jeopardised.

Nonetheless, the theory still has ardent defenders. Ivan Fesenko of Westlake University in China argues that Scholze’s assessment is “totally wrong” and that, given enough time, a clean Lean proof will emerge.

For now the mathematical community remains in a kind of limbo. The ABC conjecture sits on a precipice between celebrated breakthrough and alleged illusion, and the ongoing debate illustrates how even the most powerful computers cannot shortcut the need for human insight when a proof is built on entirely new concepts.