OpenAI宣称其下一代AI模型攻克了包括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的原始定义；证明过程仅适用于部分情况却被误用于整个群；或者代码中的群与说明文档中描述的群并非同一对象。
**37000行代码的逐行排查**
为了验证结论，Nielsen做了一件极其耗费精力的事。他建立了一张对照表，将每个数学对象在新代码中的名称和行号一一对应，例如零上闭链群位于第13700行，扭曲群位于第14069行。他还追踪了证明ICC的整条推理链：该链从第31430行起步，层层递进，最终在第31610行合成结论。
Nielsen发现，这些引理处理的是经过对偶变换后的对象，而非原始的带中心元素的群，因此并未直接覆盖到关键元素。至于它们是否对最终定理中的具体群成立，取决于两块构造之间的接口如何对接。这说明问题出在“要证明什么”上，而非“证明过程是否正确”，而Lean内核仅负责验证后者。
对于另一个扭曲的群，Nielsen表示态度较为保守。他承认代码中的引理有可能确实证明了其满足ICC，但这并不改变最终结论，因为至少有一个条件已经不满足。他将自己的两条反驳也写成了Lean代码，并在Lean 4.32.2下成功编译。
**机器检查的是形式，而非意思**
论文最后一节将此事置于更大的背景下讨论。Lean内核能保证的是证明在形式上的严丝合缝，却无法判断该证明是否真的对应了原结论。陶哲轩曾指出，验证的是形式陈述本身，而非陈述与意图的一致性，因此人类的审查不可替代。
历史上已有类似先例。一份针对五个常用Lean基准的审计发现了4833条问题，包括反例、空洞定理和不可靠公理，这些均通过了机器验证，直到人类构造出反例才被揭穿。在统计学习理论的形式化工作中，最危险的情形被称为“对错误陈述的成功证明”。张量网络研究也曾记录过类似现象：系统给出的证明在形式上完全正确，但证明的命题比预期的要弱。
Nielsen指出，OpenAI那份形式化证明可能确实正确地建立了它声称的每一条结论，但它未能建立、Lean内核也无法检查的，是这些结论与猜想原话之间的关系。Connes刚性猜想目前依然开放。论文链接及参考链接已附上。