Thirteen years of stalemate may finally have a referee. As New Scientist reports, two independent projects are now using the proof-assistant language Lean to machine-verify Shinichi Mochizuki’s 500-page claimed proof of the ABC conjecture — one of them having operated in secret for more than two years. If Lean delivers a verdict, it will be the most consequential use of formal verification in modern mathematics. And for anyone in AEC who relies on algorithmic outputs to make structural, regulatory, or compliance decisions, the implications reach well past number theory.

←TODAY: Two Lean formalisation projects are running now; Mochizuki himself has endorsed Lean as the only technology capable of resolving the dispute without social or political interference.
→3012: Zurich-3012 building permits are machine-issued against formally verified structural proofs; no human sign-off loop exists.
Fulcrum: The moment a computer outranks a Fields Medal winner in mathematical authority is the moment algorithmic trust becomes institutional infrastructure.

The backstory is worth knowing precisely. In 2012, Mochizuki posted his proof online, built on an entirely self-contained theoretical framework he called Inter-universal Teichmüller theory (IUT). The framework required years of prerequisite study just to approach. Broad mathematical comprehension never arrived. Then in 2018, Peter Scholze (University of Bonn) and Jakob Stix (Goethe University Frankfurt) — both leading figures in European mathematics, Scholze a 2018 Fields Medal laureate — announced they had identified a specific potential error. Mochizuki’s Kyoto circle maintained the proof was correct. The wider community concluded it was at best indecipherable. The stalemate calcified.

What broke the deadlock — or at least opened a door — is the maturation of proof formalisation. Tools like Lean, Coq, and Isabelle translate written mathematical arguments into machine-checkable code that either compiles or does not. There is no room for “I think this step is plausible.” Lean in particular has already been used to verify major contemporary results: Scholze himself used it for the Liquid Tensor Experiment, a high-profile formalisation of his own work in condensed mathematics. That history makes his implicit endorsement of the method, even as a skeptic of IUT, a structurally important signal. Mochizuki’s own statement — 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” — is an unusually direct thing for a mathematician to say about software.

The secrecy around one of the two projects is telling. Whoever is running it chose to work without public scrutiny for over two years, which suggests either institutional caution about premature findings, sensitivity about the political temperature of the dispute, or both. No names, no interim results, no timeline have been confirmed publicly. That opacity is itself a data point: the stakes are high enough that the project managers decided the risk of a leaked half-result outweighed the benefit of open science.

Atelier: The BIM parallel is exact, not metaphorical. When a parametric model becomes too complex for peer review — when no single engineer on a project can hold the full logic of a 15,000-element Grasshopper script in their head — the verification question is identical to the one facing Mochizuki’s reviewers. Lean’s approach (machine-checkable, rule-based, unambiguous) is structurally the same as clash detection or code-compliance checking in a BIM workflow. If formal verification can settle a 13-year dispute between Fields Medal winners, the case for bringing that methodology into structural certification and regulatory sign-off in Switzerland and the EU becomes considerably harder to dismiss.

The risk worth naming plainly: a Lean verification is only as reliable as the formalisation itself. Translating 500 pages of IUT into machine code requires human choices at every step — which definitions to use, how to bridge informal mathematical intuition into formal syntax. A formalisation can be internally consistent and still miss the mathematical point. The computer does not understand the conjecture; it checks the code. That gap is real, and anyone tempted to treat a successful Lean compilation as a final verdict should read the Lean documentation, not just the press release.

For Swiss and DACH professionals: ETH Zürich and EPFL both have active research in formal methods and proof-assistant tooling, though no confirmed direct involvement in either IUT project has been reported. The European institutional weight in this story — Scholze in Bonn, Stix in Frankfurt — means any resolution will land in a research culture that overlaps directly with Swiss academic networks. Watch the preprint servers. When one of these projects goes public, it will not be a quiet announcement.

Start here: the Lean proof assistant is open source and documented at leanprover.github.io. If your office is running complex parametric or structural scripts that no single team member can fully audit, spend thirty minutes understanding what formal verification actually does. The ABC conjecture may be abstract; the verification principle is not.

Source: New Scientist