14年ABC猜想僵局，Lean正在撬开一道缝

2012年8月的一个普通下午，京都大学的望月新一悄悄在学校网站上挂出四篇总计500页的论文。没有新闻发布会，没有同行预印本，这位此前在数论界寂寂无闻的数学家，宣称自己用一套自创的「宇宙际Teichmüller理论」（IUT），证明了困扰学界27年的ABC猜想。

这是数论领域堪比「费马大定理」的圣杯级难题，却因为IUT理论的极度晦涩——望月自己估计需要10年专业训练才能看懂——彻底引爆了数学界的分裂。顶尖数学家们花了6年试图理解证明，最终在2018年陷入死局：一方认定证明存在致命漏洞，另一方坚称批评者根本没读懂理论。这场僵局持续到今天，直到一款叫Lean的计算机工具，终于让双方找到了对话的可能。

为什么Lean能打破14年的僵局？

你可以把传统数学证明想象成一份只有步骤没有食材的菜谱：写菜谱的人默认你知道「少许盐」是多少，「中火煎熟」要多久，同行评审靠的是经验和默契。但望月的IUT理论，相当于用一套没人见过的厨具和食材写菜谱——连「少许」「中火」都是他自创的定义，自然没人能复刻出成品。

而Lean，就是把这份模糊菜谱翻译成机器能执行的精确指令：每一勺盐的克数、每一秒的火候、每一步操作的逻辑依据，都必须用代码写死。它的核心是一个极小的「可信内核」——只有约1万行代码，经过全球数学家和计算机科学家反复验证——任何证明只要通过这个内核的检查，就意味着逻辑上绝对自洽，没有任何模糊空间。

具体到ABC猜想的证明，Lean的作用分三层：首先，它要求把IUT理论里所有自创的概念，都翻译成数学界通用的形式化语言，相当于给望月的「私人厨具」贴上通用标签；其次，它会自动检查每一步推理的逻辑链条，从最基础的公理到最终的结论，绝不允许任何省略或跳跃；最后，它把整个500页的证明拆成一个个可验证的小模块，就像把一本厚书拆成一页页纸，方便数学家们逐页检查——尤其是那个被质疑了8年的核心推论Corollary 3.12。

卡在那道坎上的两个团队

2023年底，日本ZEN数学中心发起了LANA项目——一群既懂IUT理论又会用Lean的数学家，试图中立地把望月的证明形式化。团队里的亚当·托普拉斯说，他们花了一年半时间，终于把证明拆到了那个争议核心，然后就卡住了。

这个坎，正是2018年德国数学家 Scholze 和 Stix 指出的漏洞：望月在推导Corollary 3.12时，用到了两种不兼容的「测量尺度」，就像用米尺和英尺同时量一张桌子，最后得出的长度却被当成了同一个数值。LANA团队反复核对了所有步骤，甚至通过中间人向望月请教，但始终无法理解两种尺度如何统一。

另一边，望月自己的团队也在做Lean形式化，但他们的目标不是「验证正确性」——望月坚信证明没问题——而是「消除误解」。他们先从那个争议推论入手，已经写出了70行Lean代码。但帝国理工学院的凯文·巴扎德直言：「70行连本科生定理都证明不了，更别说500页的IUT了。」

现在的局面像一场拔河：LANA团队站在数学界的通用逻辑里，试图把望月的证明拉进可理解的范畴；望月团队则站在IUT的独特逻辑里，试图用Lean证明自己的理论本身没有矛盾。双方都卡在了同一个点，但方向完全不同。

AI正在给Lean装上加速引擎

单靠人力，把500页的IUT证明翻译成Lean代码，可能需要几十位专家花上十年。但AI的加入，正在把这个时间大幅缩短。

2024年以来，DeepMind的AlphaProof、字节跳动的SEED Prover等工具，已经能把自然语言的数学证明自动翻译成Lean代码，准确率超过80%。它们就像专业的翻译官，能把望月的「私人语言」快速转换成Lean能理解的代码，数学家只需要在旁边修正细节。更关键的是，AI能自动发现证明中的逻辑漏洞——比如两种测量尺度的不兼容——它会在代码编译时直接报错，绝不给模糊空间留余地。

不过AI也有局限：它只能在已有的逻辑框架内工作，没法像望月那样创造出全新的数学概念。就像一个顶级翻译官，能把外文小说翻得精准流畅，但没法写出一本全新的小说。所以这场僵局的最终突破，依然需要数学家的创造力——要么LANA团队找到理解两种尺度的新角度，要么望月团队用Lean证明这两种尺度的兼容性。

这场持续14年的争议，本质上是数学界的一个终极问题：当一个证明复杂到只有创造者自己能理解时，它还算不算「证明」？

Lean给出的答案是：证明的正确性，不该依赖于人的理解，而应该依赖于逻辑的自洽。不管望月的IUT理论多么晦涩，只要能通过Lean的验证，就意味着它在逻辑上是成立的；如果通不过，那问题出在哪一步，也会被精准定位。

逻辑的尽头，才是数学的真相。

或许用不了多久，Lean会给出一个明确的答案——不管是证明望月正确，还是指出他的错误——但更重要的是，它给数学界留下了一个全新的共识：再复杂的理论，也该用逻辑说话，而不是用权威或资历。