AI宣称推翻Connes猜想 人类数学家：37000行代码反例不成立

近期，OpenAI推出的新一代人工智能模型宣称攻克了十项世界级数学难题，其中一项标志性成果是推翻了Connes刚性猜想。不过仅仅时隔一天，来自堪萨斯大学拓扑物理中心的J. L. Nielsen就发表了针对性学术回应，明确指出AI提出的反例并不成立。

为了验证AI的结论，Nielsen对OpenAI公开的37000行Lean 4代码进行了逐行回溯，将每一个数学对象还原到其原始数学原型，最终梳理出两条互相独立的错误路径，直指AI的证明存在漏洞。

要理解这场学术交锋，首先需要明确Connes刚性猜想的核心内容。在数学领域中，我们可以为群结构匹配对应的代数体系，有时两个外观不同的群，却能生成完全一致的代数结构。1980年左右，数学家Connes提出了一个猜想：只要一个群满足ICC和Kazhdan性质(T)这两个附加条件，那么只要二者生成的代数结构相同，这两个群本身就必然是同构的。换句话说，想要推翻这个猜想，就必须找到一组满足两个附加条件，但构造方式完全不同的非同构群。

OpenAI的新一代AI模型正是按照这一思路展开工作：它构造了两个非同构的群，证明二者可以生成相同的代数结构，同时还验证了这两个群都满足ICC和Kazhdan性质(T)。整套论证被整理为37000行Lean 4代码，通过了Lean内核的逐条形式化验证，同时还附带了一份说明文档，解释了两个群的具体构造方式。

但Nielsen在仔细审查代码后发现，AI构造的其中一个群，实际上并没有满足猜想要求的两个附加条件——既不满足ICC，也不具备Kazhdan性质(T)。她进一步指出了三种可能的错误源头：一是代码中对Kazhdan性质(T)的定义没有忠实还原原始数学定义；二是证明过程仅在局部成立，却被错误推广到了整个群；三是代码中实现的群与说明文档里描述的群并不一致。

为了严谨地验证自己的结论，Nielsen还完成了一项工作量极大的工作。由于OpenAI公开的代码是整合后的单文件版本，早期分模块源码中的变量名和模块名都已经被简化隐藏，她专门制作了一份详细的对照表，将每个数学对象在新代码中的名称和对应的行号一一对应标注：比如零上闭链群位于第13700行，扭曲群位于第14069行，两套代数同构的证明位于第36712行，主定理则位于第36954行。

除此之外，她还完整追溯了代码中证明ICC条件的整条推理链：这段证明从第31430行开始，经过逐层的逻辑推导，最终在第31610行合成了最终结论。Nielsen指出，这段推理链处理的是经过对偶变换后的对象，而非原始的带有中心元素的群，因此并没有直接覆盖到证明所需的关键元素。至于这些推导是否能完全适用于最终进入定理的具体群，则取决于两块构造模块之间的接口对接方式。

这一问题的核心在于，它并非“证明过程是否正确”的问题，而是“要证明的目标是否正确”的问题。Lean内核只能验证证明过程在形式上是否严谨自洽，但无法验证这个形式化证明是否真正对应了原始的数学猜想。正如Nielsen所说，人类在阅读猜想时会自动关注前提条件，但证明助手只会对给定的形式陈述进行验证，即便该陈述并不满足原始猜想的前提，也会照常验证基于它的所有断言。

对于另一个被构造的扭曲群，Nielsen采取了保守的态度。她表示自己并没有从代码中独立核实该群是否满足ICC条件，也承认代码中的引理有可能确实证明了这一点，但只要存在一个群不满足附加条件，AI的反例就无法成立，因此这并不影响最终的结论。

值得一提的是，Nielsen还将自己的两条反驳意见整理为Lean代码，并在Lean 4.32.2版本下完成了编译通过。

在论文的最后部分，Nielsen将这一事件放在了更广阔的学术背景中进行讨论。她指出，Lean这类形式化证明工具所能保证的，仅仅是一段证明在形式上严丝合缝，却无法验证这段证明是否真正证明了原始的数学结论。这一观点也可以引用数学家陶哲轩的说法：形式化验证只能证明形式陈述本身的正确性，而无法确认该陈述是否与我们的原始意图相符，因此人类的学术审查无法被完全替代。

类似的问题在学术史上早有记录。一份针对五个常用Lean基准的审计工作就发现了4833条问题，包括反例、空洞定理和不可靠公理，而这些内容都通过了机器验证，直到人类学者构造出具体的反例后，才发现被证明的陈述本身就是错误的。

在统计学习理论的形式化工作中，最危险的情形被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。张量网络领域的相关研究也记录过同类现象：系统生成的证明在形式上完全正确，但它所证明的命题比研究者最初预期的要弱得多。

Nielsen总结道，OpenAI的形式化工作可能在每条单独的结论上都做到了正确，但它无法证明这些结论与Connes刚性猜想的原话存在关联——这正是人类审查不可替代的核心原因。

截至目前，Connes刚性猜想仍然处于未被解决的开放状态，这场AI与人类数学家的学术交锋，也为人工智能辅助数学研究的可靠性敲响了警钟。

相关论文地址：
https://philarchive.org/archive/NIEWTCv17

参考链接：
[1] https://openai.com/index/ten-advances-in-mathematics/
[2] https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean