Mathematician Rebuts OpenAI's Claimed Disproof of Connes Rigidity Conjecture Within 24 Hours
OpenAI announced that its next-generation AI model solved 10 world-class problems, including a disproof of the Connes Rigidity Conjecture, supported by 37,000 lines of Lean 4 code. Within 24 hours, mathematician J. L. Nielsen from the University of Kansas published a paper arguing that the AI's counterexample is invalid: one of the constructed groups fails to satisfy the ICC and Kazhdan property (T) conditions. Nielsen traced the entire codebase object by object, identifying two independent failure paths, highlighting the continued necessity of human review for AI-generated mathematical results.
Coverage timeline
量子位量子位
数学家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的整条推理链追了一遍
