Lean 确认 Mochizuki 的 ABC 证明存在漏洞

Gap in Mochizuki's proof of ABC confirmed by Lean

经过两年的努力，LANA 项目团队在今天召开新闻发布会，正式宣布了一个关键结论：Mochizuki 在 IUT 论文中从 Theorem 3.11 推导到 Corollary 3.12 的论证方式无法被形式化。这意味着 Lean 等自动验证工具无法通过该证明。不过，鉴于 Mochizuki 近期对该点的解释正在演变，团队决定暂时保留最终判断。此次会议还展示了 LANA 项目的重要成果：一份由外部数学家撰写的、面向公众的 IUT 理论关键论证分析，并与 2018 年 Scholze-Stix 报告进行了对比。这一进展为数学界理解 ABC 猜想证明的争议提供了新的视角。

"IUT 论文中从 Theorem 3.11 到 Corollary 3.12 的论证方式无法被形式化。"