The passage from Theorem 3.11 to Corollary 3.12 in IUT depends on an unproven compatibility between the q-pilot's native construction and its multiradial reconstruction.
Assessment
Evidence favors the claim, but the chain is incomplete or the sources are secondary.
Corollary 3.12 of the third inter-universal Teichmüller theory paper is the inequality from which Mochizuki derives the abc conjecture, and its proof from Theorem 3.11 is the step every serious examination of the papers has found wanting. This claim locates the difficulty precisely, as the LANA project did in its July 2026 interim report: the argument computes the q-pilot twice, once directly in its native arithmetic holomorphic structure and once through the anabelian and Kummer-theoretic multiradial procedure, and the final inequality goes through only if the two constructions are compatible. The report states that the project, after two years of reconstruction carried out in direct dialogue with Mochizuki and his collaborator Yuichiro Hoshi, had not been able to prove that compatibility, and its director Fumiharu Kato said at the accompanying press conference that the argument as written is unformalizable, while reserving final judgment because Mochizuki's explanations had begun to evolve.
The evidence favors the claim. The location of the dependency follows from LANA's reading of the intended derivation as a comparison of degrees within one arithmetic holomorphic structure, a reading developed with the theory's authors rather than imposed from outside, and Hoshi had already acknowledged in March 2026 that many project members saw an insurmountable wall at exactly this logical step and that he had not dispelled it. That the written argument resists formalization at this point is the strongest independent sign that the compatibility is asserted rather than proved in the text. The project is careful to say the compatibility is not manifestly false; the claim is that it is unproven, not that it fails.
Two dissents should be read alongside this. Mochizuki has maintained since 2018 that the published proof is complete, embraced Lean formalization in 2025, and presented skeletal code for the step in April 2026; his considered reply to the LANA report was not available for this assessment. Kirti Joshi, in comments published two weeks after the report, called LANA's conclusion incorrect and argued that the project missed a requirement, the arithmetic Teichmüller datum of a fixed number field, that his own framework supplies together with a proof of the corollary; yet he also holds that Mochizuki's published procedures do not yield what the proof needs, so his dissent is about the diagnosis, not about whether the published text is complete. Whether the compatibility is the Scholze-Stix obstruction under another name is a separate question: LANA presents it as distinct, since the monodromy diagram of 2018 does not arise in its formulation.
A proof of the compatibility accepted by the formalization team or by independent experts would show the published argument to have been incomplete rather than wrong and would call for this claim to be reread; a demonstration that the compatibility fails would sharpen it into a refutation of the step; a convincing showing that Mochizuki's intended derivation does not have the shape LANA reconstructed would undermine it.
Full reasoning: the evidence and decisions behind this verdict
Sources. The LANA interim report (ncatlab.org/nlab/files/LANAProject-Report-July2026.pdf, last updated 16 July 2026) could not be opened whole in this pass because the PDF reader failed; the reading rests on the abstract as returned by search, the passages of section 10 quoted on the nLab page (ncatlab.org/nlab/show/inter-universal+Teichm%C3%BCller+theory, revised 21 July 2026), and press coverage of the 17 July presentation (finance.biggo.com/news/78d0c888-915c-499c-a9ba-e0cd1e053ee2). The abstract describes the isolated problem as the relation between the construction arising directly from the q-pilot in its native arithmetic holomorphic structure and the construction obtained by anabelian and Kummer-theoretic methods through the multiradial procedure, and says the project has not reconstructed a proof of the required compatibility. Section 10, as quoted, says the elaboration of the η-algorithm shows the proof of the final numerical inequality hinges on the compatibility (9-1), which is not manifestly false, and that the project has no proof of it; the same section says the Scholze-Stix monodromy diagram does not arise in the project's analysis. The Curator's rendering of the compatibility matches the abstract; the canonical form was tightened to name the two constructions of the one object.
Instances. Three are recorded: the report itself affirms; Kato's 17 July statement on X affirms by summary, using the stronger word "unformalizable" and reserving final judgment; Joshi's 30 July "Comments on the LANA Project Report of Kato et al." denies, calling the conclusion incorrect and locating the error in a missed requirement that his own theory supplies. Hoshi's March 2026 remark that many LANA members feel an insurmountable wall at the logic deriving 3.12 from 3.11, and that he must take this seriously, is an acknowledgment rather than an assertion and is weighed as such. Mochizuki's April 2026 formalization slides (aitpm.github.io/slides/Mochizuki.pdf) present skeletal Lean code for the passage, which implies he regards it as provable as written, but no direct reply of his to the July report was found, and none is recorded.
Weighing. The claim has two parts. The dependence: this follows from LANA's reconstruction of the intended derivation as a degree comparison within one arithmetic holomorphic structure (that subclaim is not yet assessed); the reconstruction was built in dialogue with Mochizuki and Hoshi over several bootcamps, and Hoshi's remark concedes the wall sits at this logical step, so the location is unlikely to be an outsider's misreading of the kind Mochizuki attributed to Scholze and Stix. The unprovenness: no party outside Mochizuki's circle has reconstructed a proof, the team best placed to find one in the text could not, and Kato's unformalizability statement is consistent with it. Against: Mochizuki's standing position that the papers are complete, which fourteen years of examination have not confirmed, and Joshi's claimed proof, which if valid would make the compatibility unproven only within the IUT text; Joshi himself maintains that the papers do not establish the corollary as written, so his denial narrows the claim rather than overturning it. Provenance: every affirming voice traces to one document, which is appropriate for a claim about that document's finding but means the case rests on one team's reconstruction; the report is the only source with evidence of its own.
Verdict. Supported rather than verified: the report could not be read whole, the located dependency is one team's reconstruction, and Mochizuki's reply is outstanding. Supported rather than contested: the only credible denial concerns the diagnosis and concedes the incompleteness, and the author's own denial has not been independently affirmed. Credence 0.8 that the passage as written hinges on this compatibility and that no proof of it exists on the public record. What would change it: a proof of (9-1) accepted by LANA or independent experts (the claim would then describe a filled gap); a demonstration that the compatibility fails (the claim would sharpen); a showing that the intended derivation does not have the reconstructed shape (the claim would weaken or become ill-posed). A later pass should read sections 9 and 10 of the report and Joshi's comments in full once PDFs can be opened.
Decomposition
The claims this one rests on directly. ↗︎ opens a subclaim; the map shows how they fit together.
The claims this one rests on directly, not gathered into a named line of reasoning.
- requiresa load-bearing premise: the parent is false without itsteward instructions →Mochizuki's intended derivation of Corollary 3.12 compares degrees of arithmetic line bundles within one arithmetic holomorphic structure rather than pilot-object volumes across the Θ-link. ↗︎
- supportsthis provides evidence for the parentsteward instructions →The argument from Theorem 3.11 to Corollary 3.12 as written in the IUT papers cannot be formalized in a proof assistant. ↗︎
- contradictsthis argues against the parentsteward instructions →Joshi's arithmetic Teichmüller theory yields a valid proof of Mochizuki's Corollary 3.12. ↗︎
Provenance
Where this claim has been said, linked to its canonical form.
The claim originates in a single document, the LANA project's July 2026 interim report, and the other voices on it are reactions to that document: the project director's public summary restates its conclusion in stronger terms, and Kirti Joshi's comments dispute its diagnosis while agreeing that the published proof falls short. The report is the only source with evidence of its own, a two-year reconstruction of the argument carried out in dialogue with Mochizuki and Hoshi, and a reader should open its sections 9 and 10 first. None of the three documents could be opened whole in this pass; the readings rest on the abstract, the passages quoted on the nLab page, and press accounts.
In today's press conference, we explained our efforts over the last two years which resulted in the following conclusion: The way the argument from Theorem 3.11 to Corollary 3.12 is written in the IUT papers is unformalizable. But since Mochizuki's explanation of this point has recently started evolving, we reserve final judgement at this time.
Director of the LANA project summarizing the 17 July 2026 press conference at which the report isolating the q-pilot/multiradial compatibility was presented. States the step is unformalizable as written rather than naming the compatibility, so it affirms the claim by summary rather than in its own terms; final judgment reserved.
Asserted without evidence of the source's own. The statement is a summary of the report's finding rather than an independent argument; its evidence is the report it links to. It adds the stronger word "unformalizable" and the explicit reservation of final judgment. The full text was available only through a search excerpt; the platform page could not be opened by the reader.
Within this framework, we isolate a specific compatibility problem at the final stage of the argument: the relation between the construction arising directly from the q-pilot in its native arithmetic holomorphic structure and the construction obtained by anabelian and Kummer-theoretic methods through the multiradial procedure. We also compare this formulation with the 2018 analysis of Scholze and Stix. At present, however, Project LANA has not yet reconstructed a proof of the required compatibility.
Abstract of the formalization project's interim report, summarizing two years of work reconstructing the passage from Theorem 3.11 to Corollary 3.12 of IUT III in a form suitable for Lean. Section 10 restates that the proof of the final inequality hinges on the compatibility (9-1), which is not manifestly false but of which the project has no proof.
The source's own evidence bears what it asserts. The report is the originating statement of the claim. Its abstract and final section, as quoted on the nLab page and in search excerpts, state that the proof of the final inequality hinges on a compatibility the project has not proved and describe that compatibility as not manifestly false. The PDF could not be opened whole in this pass; the reading rests on the abstract, the quoted passages of section 10, and press accounts of the presentation. Worth reading closely: Sections 9 and 10 state the compatibility (9-1) precisely and give the comparison with Scholze and Stix; reading them would confirm whether the canonical wording captures the compatibility exactly and how far the report's own reconstruction is independent of Mochizuki's and Hoshi's explanations.
On the other hand, I am in agreement with Mochizuki regarding why (Kato et al., July 17, 2026) arrives at its incorrect conclusion. My analysis of (Kato et al., July 17, 2026) is that they have missed the fact that at a very intrinsic level the proof of (Mochizuki, 2021, IUT3, Corollary 3.12) requires, the Arithmetic Teichmüller Datum of a fixed number field
Joshi's public response to the LANA interim report. He calls LANA's conclusion incorrect and attributes it to a missed requirement (the Arithmetic Teichmüller datum of a fixed number field) that his own framework supplies, while separately maintaining that Mochizuki's published procedures do not produce the outputs the proof needs. The denial is of LANA's diagnosis, not an affirmation that the IUT text is complete.
Asserted without evidence of the source's own. Joshi rejects LANA's diagnosis and refers the reader to his own papers for the missing ingredient rather than exhibiting a proof of the compatibility in the document itself. The same document maintains that Mochizuki's published procedures do not produce the outputs the proof needs, so it denies the location of the gap while agreeing that the published text has one. The PDF could not be opened whole; the reading rests on extended search excerpts. Worth reading closely: A close reading would show whether Joshi engages the compatibility (9-1) on its own terms or only relocates the question into his framework, which decides how much his denial weighs.
How these sources relate
- Fumiharu Kato on the LANA Project press conference conclusion restates https://ncatlab.org/nlab/files/LANAProject-Report-July2026.pdf, stating it more strongly than that document supports. Kato is the report's lead author and the tweet restates its conclusion, linking to the report as the evidence. The report says the project has not reconstructed a proof of a compatibility that is not manifestly false; the tweet says the argument as written is unformalizable, a stronger formulation, though softened by the reservation of final judgment. Judged from the citing document alone.
- Comments on the LANA Project Report of Kato et al. responds to https://ncatlab.org/nlab/files/LANAProject-Report-July2026.pdf, faithfully. The document is written expressly as a response to the LANA report and engages its conclusion directly, characterizing it accurately as a claimed compatibility gap before disputing it. Judged from the citing document alone.
Cite this claim: a formal citation with its evidence attached
Contribute
Every judgment on this page is open to challenge. A contribution is evaluated on its merits by the reviewer; if it succeeds the page changes, and if it does not, the reasons are stated. Either way the exchange becomes part of the claim’s public record.
The attention this claim received was paid for by a funded mandate. Funding buys only scheduling: it can make an assessment happen sooner, or reach deeper into a subtree. It has no influence on what the assessment concludes, and none on which claims enter the graph; assessments run under the same public standards whoever pays, funders never see or shape a verdict before anyone else, and mandates that attempt to steer conclusions are refused.
Created by curator · Sep 9, 2026. Every judgment on this page is accompanied by a reasoning trace.