The secret project to settle controversial maths proof with a computer
New Scientist · rss · 2026-04 Reader 🖥️
Two independent projects are now attempting to formalise Shinichi Mochizuki's contested proof of the ABC conjecture using the Lean proof assistant, offering the first real hope of resolution since the controversy began in 2012 -- but the secret project (LANA) has already hit a roadblock at the exact point critics originally flagged.
theoretical · science journalism / narrative report — A news feature reporting on two concurrent formalisation efforts aimed at resolving the ABC conjecture proof controversy. The article is expository, not itself a mathematical argument.
Structure
| Part | Role |
|---|---|
| Background: the ABC conjecture and Mochizuki's 2012 proof | Sets up the problem -- a 500-page proof using novel IUT theory that the community could not verify |
| The impasse: Scholze-Stix objection (2018) and community split | Establishes why formal verification is needed -- human dialogue failed to resolve the dispute |
| Mochizuki's olive branch: endorsement of Lean formalisation (2025) | Explains the enabling condition -- Mochizuki's own willingness to engage with formalisation |
| The LANA project: secret effort, progress, and roadblock | Central narrative -- a two-year covert formalisation attempt that got stuck at the same controversial point |
| Mochizuki's own formalisation project | Counterpoint -- Mochizuki frames formalisation as communication, not verification; 70 lines of code so far |
| Assessment from Buzzard and Topaz: cautious optimism | Evaluative coda -- experts see the dialogue itself as the most promising development |
Key terms
- ABC conjecture
A number-theory conjecture about the relationship between prime factors of integers a, b, c satisfying a + b = c - Inter-universal Teichmuller theory (IUT)
The novel mathematical framework Mochizuki invented to prove ABC; the source of the controversy because it is difficult to understand - Formalisation (in Lean)
Translating a written mathematical proof into machine-checkable code so its correctness can be verified automatically - LANA project
Lean and Anabelian geometry project, a secret initiative led by Kato Fumiharu to formalise Mochizuki's proof and settle the controversy - Blueprint
A structured plan for formalisation, breaking the proof into stages that can be incrementally verified
Propositions
- explicitFormal verification in Lean is the most promising path to resolving the ABC conjecture proof controversy.conf: high
- explicitThe LANA project got stuck at the same point Scholze and Stix identified as potentially erroneous in 2018.conf: high
- explicitMochizuki views the formalisation exercise primarily as a communication tool rather than a correctness check.conf: high
- implicitThe disputed point in the proof may contain a genuine gap or error, not merely a communication failure.conf: medium
- explicitMochizuki's 70 lines of Lean code represent a negligible fraction of what would be needed to formalise the full proof.conf: high
Arguments
Lean formalisation can resolve the ABC controversy where human dialogue could not. strength: medium
Explicit premises:
- Human attempts to clarify the proof (2012-2018) reached an impasse.
- Lean produces a machine-checkable record immune to misinterpretation.
- Both Mochizuki's camp and external mathematicians are now engaged with Lean.
Implicit premises:
- A machine-verified proof would be accepted as definitive by both sides of the dispute.
- The disputed step in IUT is expressible in Lean at all (i.e., formalisation is technically feasible for IUT's novel constructions).
Inferences:
- If the proof can be formalised, correctness is settled; if formalisation gets stuck at the disputed point, that itself is informative.
The fact that LANA got stuck at the Scholze-Stix point strengthens the case that the proof has a genuine gap there. strength: medium
Explicit premises:
- LANA independently arrived at the same problematic point that Scholze and Stix flagged.
- LANA spent 1.5 years and multiple workshops trying to resolve it without success.
Implicit premises:
- Independent convergence on the same obstacle is evidence that the obstacle is in the proof, not in the readers.
- If the argument were merely hard to understand (not flawed), sustained expert effort should eventually clarify it.
Inferences:
- The disputed passage is more likely to contain a real error than a mere communication difficulty.
Narratives
- A lone mathematician publishes a revolutionary but incomprehensible proof; the world's experts cannot determine if it is right or wrong; after a decade of deadlock, two secret and competing projects race to let a computer settle the question.
→ Frames the controversy as a dramatic intellectual mystery, sustaining reader interest and justifying the article's length. - Mochizuki's shift from isolation to engagement -- from refusing to travel or explain, to endorsing Lean and communicating (indirectly) with the LANA team.
→ Signals that progress is now possible because the previously intransigent central figure has opened a channel.
Questions addressed
- ⭕ Can the ABC conjecture proof controversy be resolved?
Two Lean formalisation projects are under way, offering the best prospect yet, but no resolution has been reached. - ⭕ Is Mochizuki's proof of the ABC conjecture correct?
Still unknown. The LANA project's roadblock at the Scholze-Stix point is suggestive but not definitive. - ✅ Why has nobody been able to verify or refute the proof in over a decade?
IUT introduced entirely novel concepts and techniques; human attempts at clarification reached impasse; social and institutional dynamics (Kyoto vs. rest of community) compounded the difficulty. - ⭕ What role can formal verification play in mathematical disputes?
The article implicitly argues it is the only viable arbiter, but this is demonstrated only if formalisation succeeds.
Gaps
- evidentialThe article does not describe what the specific disputed point in IUT actually is, even at a high level. The reader cannot assess the nature of the obstacle.
Read next: Read Scholze and Stix's 2018 report 'Why abc is still a conjecture' for details on the contested Corollary 3.12. - perspectivalNo voice from a mathematician who believes formalisation will fail or is the wrong approach. The article presents only optimistic assessments.
Read next: Seek critical perspectives on whether IUT's novel category-theoretic constructions can even be expressed in Lean's type theory. - implicit_premiseThe article assumes that a machine-verified proof would end the social controversy, but it is possible that disagreement could shift to whether the formalisation faithfully captures IUT's intended meaning.
Read next: Consider philosophical literature on the relationship between formal and informal proof (e.g., Avigad, Azzouni on formalisation and mathematical practice). - temporalNo timeline or estimate is given for how long full formalisation might take. Major formalisation projects (e.g., Liquid Tensor Experiment) have taken years for far shorter proofs.
Read next: Compare with timelines of completed Lean formalisation projects (Liquid Tensor Experiment, Sphere Eversion, FLT-regular).