A 500-page proof that no one has managed to read to the end
Imagine that a mathematician publishes, overnight, a proof of one of the hardest problems in their field — and that, twelve years later, no one has yet been able to say whether it is right or wrong. This is exactly what has been happening since 2012 with the abc conjecture, and it may be the greatest silent scandal in the history of modern mathematics. To settle it once and for all, researchers have decided to hand the verdict to a machine.
The abc conjecture: a simple-looking problem of extraordinary depth
Before diving into the details, let's lay the groundwork. The abc conjecture is a statement about integers, formulated in the 1980s by mathematicians Joseph Oesterlé and David Masser. Its central idea can be summed up as follows: if three integers a, b and c satisfy the equation a + b = c, then the prime factors that make up these three numbers cannot all be very small at once. In other words, a simple sum of two integers constrains the deep structure of their divisors.
This conjecture may sound harmless when put this way, but its implications are considerable: if it were proved, it would automatically entail the proof of dozens of other important theorems in number theory — the branch of mathematics that studies the properties of integers. Fermat's Last Theorem, for example, would follow from it almost as a corollary. The abc conjecture is thus a kind of keystone: to establish it is to open dozens of doors at once.
Mochizuki, the recluse of Kyoto
In August 2012, Shinichi Mochizuki, a professor at Kyoto University, published four papers totaling more than 500 pages on his personal website. In them, he announced that he had proved the abc conjecture. But the proof resembles nothing known: it rests on an entirely new theory, which Mochizuki developed alone over the course of a decade and which he calls inter-universal Teichmüller theory — or IUT for short.
The problem? This theory invents its own mathematical objects, its own notation, its own rules of the game. To understand the proof, one must first learn a language that no one else has ever spoken. Some of the brightest mathematicians in the world have tried. Many gave up after weeks or months of effort. Peter Scholze and Jakob Stix, two giants of number theory, ultimately claimed in 2018 to have identified a precise flaw in the argument — a key step in the reasoning that, in their view, does not hold up.
"We do not understand why this step is supposed to work, and we do not believe that it does." — Peter Scholze and Jakob Stix, 2018
—
Mochizuki, for his part, has maintained that his critics simply did not understand his theory. He responded at length, point by point, without ever conceding the slightest error. At that point, the dialogue stopped. Two camps formed: those who believe the proof is correct (mainly close collaborators of Mochizuki's in Japan), and those who consider it flawed. The rest of the community, the vast majority, has simply given up on deciding.
Why a proof can remain unresolved for ten years
This case illustrates a deep limitation of the system used to validate mathematics. In principle, a mathematical proof is either correct or incorrect — there is no grey area. But in practice, validation relies on peer review: other experts in the field who check every step of the reasoning. This system works very well when a proof fits within a shared language. It collapses when the proof reinvents that language from scratch.
No one is paid to spend six months learning an entire theory just to check whether it is consistent. Mathematicians have classes to teach, papers to publish, careers to build. Auditing Mochizuki's proof represents a colossal investment for an uncertain return. As a result, the proof was published in a journal — the Publications of the Research Institute for Mathematical Sciences in Kyoto, of which Mochizuki is himself the editor-in-chief, which has drawn criticism over conflicts of interest — but without ever obtaining the informal validation of the international community.
The computer as arbiter of last resort
Against this backdrop of total deadlock, a new approach has emerged: computer-assisted formal verification. The principle is as follows. Specialized software — called proof assistants — makes it possible to translate a mathematical proof into a formal language that the machine can check step by step, mechanically, without fatigue or bias. If a step does not hold, the computer detects it.
Researchers have undertaken to formalize key parts of IUT theory in one of these assistants. The goal is precise: to verify the exact step that Scholze and Stix have called into question. If the computer confirms the flaw, the debate is closed. If, on the contrary, it validates the step, the community will have to reconsider its objections.
This is not a trivial undertaking. Formalizing advanced mathematics in a proof assistant demands considerable work — sometimes years for just a few pages. But it may be the only way out of an impasse that humans alone have failed to resolve.
Lessons from a mathematical scandal
Beyond the Mochizuki case, this affair raises questions that go far beyond a single man or a single conjecture. How should the mathematical community handle radically new theories, ones that require years of learning before they can even be assessed? Who should bear the cost of verification? And if no one does, is an unread proof really a proof?
The rise of proof assistants opens up a serious avenue. Formalized mathematics can be checked by anyone with the right software. It no longer depends on the goodwill of a handful of overworked experts. Some researchers are already campaigning for major proofs to be systematically accompanied by a formal version. This would be a revolution in the way mathematics is done and passed on.
In the meantime, the machine's verdict is awaited with an impatience tinged with unease. For if the computer confirms the flaw, an uncomfortable conclusion will have to be drawn: for more than a decade, the global mathematical community was unable to validate or invalidate one of its own supposedly major results. And that is a flaw in the system, not just in a proof.
Key takeaways
For math enthusiasts
The abc conjecture is formulated precisely using the notion of radical of an integer. For an integer n, we define rad(n) as the product of all distinct prime factors of n — without regard to their multiplicities. For example, rad(12) = rad(2² × 3) = 2 × 3 = 6. The conjecture then states that for every real number ε > 0, there exist only finitely many triples of integers (a, b, c) that are pairwise coprime, satisfying a + b = c, and such that c > rad(abc)1+ε. In other words, the cases where c is "much larger" than the radical of the product abc are extremely rare. This formulation captures the idea that high powers among the prime factors of a sum are an anomaly, not the norm.
