数学家24小时内驳斥OpenAI猜想突破：‘AI每条都对，但不是原猜想了’

OpenAI声称其下一代AI模型解决了十个世界级数学问题，包括推翻Connes刚性猜想。次日，一位人类数学家发表论文，指出AI的反例是无效的。作者，堪萨斯大学拓扑物理中心的J. L. Nielsen从头到尾追踪了OpenAI的37,000行Lean 4代码，将每个对象映射回其数学原型，并确定了两个独立的失败路径。Connes刚性猜想指出，如果两个群具有相同的关联代数结构并满足两个附加条件（ICC和Kazhdan性质(T)），那么这两个群必定是同构的。OpenAI的模型构造了两个非同构的群，它们生成相同的代数，并证明了这两个群都满足ICC和性质(T)。Nielsen指出，AI构造的其中一个群实际上并不满足附加条件，既不满足ICC，也不具有性质(T)。她列出了三个可能的原因：代码中性质(T)的表示未能忠实对应Kazhdan的原始定义；证明仅对群的一部分成立却被应用于整个群；或者代码中的群并非解释文档所描述的群。Nielsen还对代码进行了逐行审查，在一张交叉引用表中列出了每个数学对象的名称和行号。她发现用于证明ICC的引理应用于对偶变换后的对象，而非带有中心元素的原始群，因此它们并未直接覆盖关键元素。她将两篇反驳写成Lean代码，并在Lean 4.32.2下编译通过。论文的最后部分讨论了更广泛的背景：Lean内核确保了形式上的正确性，但并不确保命题实际证明了预期的结论。引用陶哲轩的话，验证证明检查的是形式陈述本身，而非其与意图的一致性，因此人类审查无法被取代。过去的五项常见Lean基准审计发现了4,833个问题，包括反例、空洞定理和不可靠的公理，这些均由机器验证，而人类后来构造了反例表明这些被证明的命题是虚假的。Nielsen写道，OpenAI的形式化可能正确确立了其声称的每个结论，但并未确立——Lean内核也无法检查——这些结论是否与原猜想的措辞相关。Connes刚性猜想仍然开放。