AI宣布推翻90年数学难题，真相是工具先坏了
一个 AI 在 7 月底宣布：困扰数学家近 90 年的考拉兹猜想，被我推翻了，反例就在这里。证据是一份电脑能逐行核验的”机器证明”，看起来滴水不漏。全世界还没来得及欢呼，真相先到了——那个”反例”，是一个数学验证工具自身漏洞造出来的幻觉。更讽刺的是，这个工具存在的意义，就是让 AI 的幻觉无处遁形。
笔者今天想把这个故事从头讲清楚。它值得每个刷手机的人知道，因为它触及一个我们正在集体押注的问题：AI 说的话，到底该信几分？
先认识这道 90 年的题
考拉兹猜想，规则简单到小学生都能听懂：随便想一个正整数，是偶数就除以 2，是奇数就乘以 3 再加 1。然后对结果重复同样的操作。
举个例：从 6 开始。6 是偶数，除以 2 得 3；3 是奇数，乘 3 加 1 得 10；10 除以 2 得 5；5 乘 3 加 1 得 16；16、8、4、2、1。到 1 之后呢？1 是奇数，乘 3 加 1 又变回 4，然后 4、2、1 无限循环。所以这道题问的是：是不是不管从哪个数出发，最后都会掉进 4-2-1 这个圈？
1937 年德国数学家考拉兹提出这个问题，至今没人能证明，也没人找得到反例。计算机已经把 2 后面跟 21 个零以内（也就是 200 万亿亿）的每个数都跑了一遍，全部回到了 1。但数学家不为所动——验证再多数字也不算证明，就像看遍全世界的白天鹅，也不能证明天鹅都是白的。匈牙利数学大师埃尔德什有句名言：“数学可能还没准备好面对这类问题。” 这道题难就难在，规则简单，却像泥鳅一样抓不住。
图：考拉兹猜想的数字树——所有能在 20 步内到达 1 的数，都挂在这棵树上。来源：Wikipedia (All Collatz sequences of a length inferior to 20)
AI 的”突破”是怎么出炉的
7 月 25 日，一位叫拉马纳·库马尔的计算机科学家发布了一个代码仓库，里面是一份”反证”：一个具体的大数，据说从它出发永远回不到 1，直接推翻猜想。关键卖点在于——这份反证是用 AI 辅助写成的一份机器可验证的证明。
这里要解释一个硬核概念。数学界这些年流行一种做法：把”证明”写成一门特殊编程语言的代码，然后交给一个叫 Lean 的”证明编译器”。它像最严格的阅卷老师，把证明的每一步拆开、逐行检查，任何一步跳了逻辑，它立刻亮红灯拒绝。被它放行的证明，理论上不可能错——这不是”理论上”，这正是它的设计目标：用机器的不讲情面，替换人类审稿的疏忽和偏见。
这套东西的分量有多重？操作系统的安全内核、加密货币的底层协议、上万个数学定理，都压在这套”机器验证”上。行业里甚至把它吹成”终结 AI 幻觉”的终极手段：AI 胡说八道没关系，让机器替你把关。
所以当库马尔拿出”Lean 验证过的反例”时，懂行的人第一反应是震惊——如果证明真的通过了机器检查，那 90 年的难题就真的塌了。消息迅速传开，社交媒体的标题一个比一个响：“AI 推翻 90 年数学难题”。
真相：阅卷老师自己算错了
反转来得极快。7 月 28 日，另一位研究者把这份反证压缩成一个极小的逻辑矛盾，打开 Lean 的官方漏洞单，编号 #14576。漏洞单的标题冷冰冰：“内核接受了错误的投影，允许在没有任何前提的情况下证明假命题。”
用人话说：那个号称不可能出错的阅卷老师，在自己最核心的检查环节漏了一道手续。检查嵌套数据类型时，有一个位置没有核对”类型名是否匹配”，于是 AI 构造的那份”证明”里，藏了一个不合格的零件，从这道缝里钻了过去。机器宣布”验证通过”的那一刻，其实是在为一个幻觉盖章。
图：小数字在考拉兹规则下的轨道，全部汇入 1。来源：Wikipedia (Collatz graph, skipping 27)
接下来是全场最戏剧化的一幕。Lean 社区一直有一个”双保险”设计：除了官方阅卷老师，还有一个独立的第三方验证器（用另一门语言、由另一拨人写的），专门交叉检查官方检查的结果。这套独立性假设，是”机器验证”信任链的保险丝。
保险丝这次断了。事后分析确认：需要同时命中两个互不相关的 bug——官方内核漏了嵌套类型检查，独立验证器则在投影检查上少看了一处，两个 bug 藏在两套代码的不同角落，却被同一份”反证”恰好踩中。独立验证器的那个 bug 恰好在此前一周刚被修复，而 AI 使用的版本是修复前的。Lean 的创造者德莫拉在事后分析里写得很坦诚：作者本人相信时间点是巧合，但也无法排除 AI 在训练数据里见过那份漏洞报告。
工程上怎么判断这件事？两个独立实现被同一发子弹同时击穿，概率低到离谱——这意味着要么运气差到极点，要么这份”反证”根本就是对着漏洞精雕细琢的。德莫拉自己给了判断：“这类事情会继续发生。AI 非常擅长利用内核的健全性漏洞。” 漏洞单提交一小时后修复就推上线了，定位快说明内核架构本身是健康的；但发现它，靠的是一次 AI 的”惊人突破”。
验证者，谁来验证？
这事的余波比事件本身更值得琢磨。漏洞发现后，OpenAI 派了一位专攻网络安全的 AI 研究员协助排查，又揪出 Lean 内核里其他几处编程错误——全都修掉了。换句话说：用来防 AI 的工具，现在要靠 AI 来查自己的 bug。
而”用 Lean 验证 Lean”的项目（把验证器本身也写进被验证的体系里）目前还没覆盖到出问题的这部分代码，而且它移植的代码段里躺着同一个 bug。验证是有层次的：AI 的结果靠验证器把关，验证器靠独立的第二实现把关，第二实现靠谁来把关？每一层都多一道工序、多一分成本，但永远没有”最后一层”。这符合工程常识：“机器验证过”从来都只是一个概率属性——检查得越深、越独立，出错概率越低，但永远不等于零。
对普通人来说，这件事最大的价值是校准预期。下次再看到”AI 攻克百年难题""AI 证明某定理”的标题，可以多问一句：验证它的是人，还是机器？如果是机器，那台机器自己有没有被验证过？反过来说，也不必因此倒向”什么都不信”的虚无——这次事件里，数学本身毫发无损，考拉兹猜想依然立在那里，漏洞被公开、被修复、被写进教科书式的复盘。系统出过 bug，但系统消化 bug 的方式，正是它值得信任的原因。
信任从来都是一串随时可能断一环的链条。聪明人不会假装链条不断，只会记得定期检查每一环。这一次，AI 替我们找到了其中一环的裂缝——以一场假突破的方式。
参考链接：
- Leo de Moura 事后分析：Lean 内核健全性漏洞 #14576 的完整复盘
- Lobsters 讨论（ojcl8j）：社区对内核漏洞的讨论，48 分热帖
- Wikipedia：考拉兹猜想词条（规则、历史与验证进展）
