数学家24小时驳回OpenAI攻破的猜想：AI证对了每句话，却已与猜想无关

OpenAI宣称其下一代AI模型解决了10个世界级难题，其中一项是推翻Connes刚性猜想。消息传出仅一天，就有一篇人类论文正面回应：AI提出的反例并不成立。

这篇反驳论文的作者是堪萨斯大学拓扑物理中心的J. L. Nielsen。她把OpenAI公开的37000行Lean 4代码从头追到尾，把每一个对象对回它的数学原型，最终给出两条互相独立的失败路径。

Connes刚性猜想大致是说：数学上可以给一个群配一套代数结构，有时两个长得不一样的群，配出来的结构却完全一样。Connes在1980年前后猜测，只要群满足ICC与Kazhdan性质(T)两个附加条件，这种情况就不会发生——结构一样，群就必须一样。想反驳它，需要举出同时满足两个条件、但构造不一样的群。

OpenAI新模型的做法，正是构造两个不同构的群，让它们生成同样的代数，并给出两个群都满足ICC和性质(T)的证明。整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过，另附一份说明文档解释两个群如何搭出来。

Nielsen指出，AI构造的其中一个群其实没有满足附加条件：它既不是ICC，也不是性质(T)。她列出三种可能：代码里的性质(T)没有忠实对应Kazhdan的原始定义；证明只对部分成立却被算到整个群上；或者代码里的群根本不是说明文档描述的样子。

为了核实，她做了一件更费力的工作：公开发布的是整合成单文件的版本，早期分模块源码里的名字全部消失，于是她列了一张对照表，把每个数学对象在新代码里的名字和行号一一标出——零上闭链群在第13700行，扭曲群在第14069行，两套代数同构的证明在第36712行，主定理在第36954行。她追查ICC证明的整条推理链后发现，相关引理处理的是经过对偶变换之后的对象，而不是原来那个带中心元素的群，因此没有直接覆盖关键元素。

在Nielsen看来，问题出在“要证什么”，而不是“证得对不对”——Lean只负责验证后者。她也把自己的两条反驳写成Lean代码，并在Lean 4.32.2下编译通过。论文最后一节把这件事放进更大的背景：Lean内核能保证一段证明在形式上严丝合缝，却不负责它是否真的证明了原结论；正如陶哲轩所说，机器验证的是形式陈述本身，而不是陈述与意图是否相符，人类的审查不能被取代。

这类事故此前已有记录：一份针对五个常用Lean基准的审计给出4833条发现，包括反例、空洞定理和不可靠公理，全部通过了机器验证，最后是人类构造出反例才发现被证明的句子本身就是错的。统计学习理论的形式化工作中，最危险的状况被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。

Nielsen写道，OpenAI的形式化可能把它声称的每一条结论都建立对了，但它没有建立、Lean内核也检查不了的，是这些结论与猜想原话有没有关系。人读猜想会看到前提，而证明助手拿到一个不满足前提的结论，照样会验证关于它的任何断言。Connes刚性猜想目前仍然开放。