望月新一ABC证明遭重击：加藤团队利用Lean验证确认关键论证无法形式化

在2026年7月17日的新闻发布会上，加藤文元团队展示了他们过去两年的研究成果，指出望月新一在关于ABC猜想的IUT（宇宙际Teichmüller理论）论文中，从定理3.11到推论3.12的论证方式是“无法形式化”的。这意味着该部分逻辑无法被计算机验证系统（如Lean）严格定义和证明，从而构成了潜在的逻辑漏洞。虽然加藤团队提到，由于望月新一近期对该点的解释开始出现变化，因此他们暂保留最终判决，但目前的结论对IUT理论的有效性提出了严峻挑战。作为LANA项目的核心成果，该团队不仅利用计算机辅助验证了这一复杂数学理论，还为大众提供了一份可读性强的关键论证分析文档，并将其与2018年Scholze-Stix的批评报告进行了对比。这一事件被视为计算机形式化验证在解决顶级数学争议中发挥关键作用的里程碑。

事件分析

💡 核心观点：计算机形式化验证正在成为数学真理的终极裁决者，这一里程碑事件标志着高深数学研究范式正从人类经验共识向机器逻辑验证的彻底转型。