数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”

< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400"> 数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关” 梦晨 2026-08-04 17:22:46 来源： 量子位 第二天，就有一篇人类论文回应：AI提出的反例不成立 梦晨 发自 凹非寺 量子位 | 公众号 QbitAI OpenAI宣称下一代AI模型解决了10个世界级难题，其中包括推翻了 Connes刚性猜想 。 第二天，就有一篇人类论文回应： AI提出的反例不成立 。 作者是堪萨斯大学拓扑物理中心的 J. L. Nielsen ，她把OpenAI公开的37000行Lean 4代码从头追到尾，把每一个对象对回它的数学原型，最后给出两条互相独立的失败路径。 具体的证明过程咱一般人也看不太懂，让AI和数学家神仙打架去吧。 但通过这件事，说明人类对AI科研结果的审查仍然很关键。 什么是Connes刚性猜想 Connes刚性猜想说的是这样一件事。 数学上可以给一个群配一套代数结构。有时候两个长得不一样的群，配出来的结构却完全一样。 Connes在1980年左右提出猜测： 只要这个群满足两个附加条件，这种情况就不会发生，结构一样，群就必须一样。 这两个附加条件，一个叫ICC，一个叫Kazhdan性质(T)。 换句话说，想反驳这个猜想，需要举出满足两个条件，但构造不一样的群。 OpenAI新模型的做法是构造两个不同构的群，让它们生成同样的代数，并给出两个群都满足ICC和性质(T)的证明。 整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过，另外附了一份说明文档，解释这两个群是怎么搭出来的。 Nielsen指出： AI构造的其中一个群，其实没有满足附加条件，既不是ICC，也没有性质(T) 。 这其中有三种可能： 代码里性质(T)没有忠实对应Kazhdan的原始定义；或者证明只对部分成立，却被算到了整个群上；又或者代码里那个群根本不是说明文档里描述的样子。 37000行，逐行对号 为了验证这个结论，Nielsen还做了一件更费力的事。 公开发布的代码是一个整合成单文件的版本，早期分模块源码里的那些名字全都不见了。 她于是列了一张对照表，把每个数学对象在新代码里的名字和行号一一标出： 零上闭链群在第13700行，扭曲群在第14069行，两套代数同构的证明在第36712行，主定理在第36954行。 她还把代码证明ICC的整条推理链追了一遍。这条链从第31430行起步，一层层往上传递，最后在第31610行合成结论。 Nielsen指出的问题是，这些引理处理的是经过对偶变换之后的对象，不是原来那个带中心元素的群，因此并没有直接覆盖到关键的那部分元素。 至于它们是否对最终进入定理的那个具体的群里每一个元素都成立，取决于两块构造之间的接口怎么对接。 这说明“要证什么”就出了问题，不是“证得对不对”的问题。Lean只负责验证后者。 对于另一个扭曲的群，Nielsen的态度是保守的。她说自己没有从代码里独立核实它到底满不满足ICC，也承认代码里的引理有可能确实证明了它满足，但那不改变结论，已经有一z个群不满足。 她把自己的两条反驳也写成了Lean代码，在Lean 4.32.2下编译。 机器检查的是形式，不是意思 论文最后一节把这件事放进了一个更大的背景。 Lean内核能保证的事情，只是一段证明在形式上严丝合缝，但不负责是否真的能证明原结论。 这里可以直接引用陶哲轩的说法：验证证明的是形式陈述本身，而不是这个陈述和意图相符，所以人类的审查不能直接被取代。 过去这类事故已经有记录。 一份针对五个常用Lean基准的审计给出了4833条发现，包括反例、空洞定理和不可靠公理，全都通过了机器验证。最后是人类构造出反例，才发现被证明的那句话本身是错的。 在统计学习理论的形式化工作中，最危险情形被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。 张量网络方面的研究也记录过同类现象：系统给出的证明形式上完全正确，只是它证的那个命题比预期的要弱。 Nielsen写道，OpenAI那份形式化可能把它声称的每一条结论都建立对了。但它没有建立、Lean内核也检查不了的，是这些结论和猜想的原话有没有关系。 人读猜想会看到前提，证明助手拿到一个不满足前提的结论，会照样验证关于它的任何断言。 Connes刚性猜想仍然开放。 论文地址： 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 版权所有，未经授权不得以任何形式转载及使用，违者必究。