abc Secret Verification Project
Two Lean formalization efforts are trying to clarify the disputed 2012 claim around the abc conjecture.
The abc conjecture, formulated in 1985 by Oesterle and Masser, states that for coprime positive integers with a + b = c, the value c is bounded by a power of the radical of abc. Mochizuki claimed a proof in 2012 via inter-universal Teichmuller theory, but Scholze and Stix identified a gap in Corollary 3.12 that the broader community considers unresolved. Two parallel Lean formalization efforts emerged in the 2020s: the LANA (Lean and Anabelian geometry) project, coordinated through the ZEN Mathematics Center led by Fumiharu Kato, and a separate Mochizuki-linked formalization whose slides appeared in April 2026 at a workshop on AI and Theorem Provers in Mathematics. The goal is not a new proof but a computer-checkable determination of whether the claimed argument can be made precise.
Formula
For every ε > 0, only finitely many coprime triples violate this bound — the conjecture at the heart of the verification effort.
The product of distinct prime factors of n, stripping all multiplicity. Small rad(abc) relative to c is the 'surprise' abc measures.
Mochizuki's inter-universal Teichmüller theory claims to establish abc through this discriminant bound on elliptic curves.
Summary
The abc conjecture, formulated in 1985 by Oesterle and Masser, states that for coprime positive integers with a + b = c, the value c is bounded by a power of the radical of abc. Mochizuki claimed a proof in 2012 via inter-universal Teichmuller theory, but Scholze and Stix identified a gap in Corollary 3.12 that the broader community considers unresolved. Two parallel Lean formalization efforts emerged in the 2020s: the LANA (Lean and Anabelian geometry) project, coordinated through the ZEN Mathematics Center led by Fumiharu Kato, and a separate Mochizuki-linked formalization whose slides appeared in April 2026 at a workshop on AI and Theorem Provers in Mathematics. The goal is not a new proof but a computer-checkable determination of whether the claimed argument can be made precise.
