OpenAI攻破数学猜想24小时被人类驳回，37000行形式化证明遭逐行审查

事件概述

OpenAI此前宣称下一代AI模型解决了10个世界级数学难题，其中包括推翻Connes刚性猜想。然而第二天，堪萨斯大学拓扑物理中心的J. L. Nielsen发表论文回应：AI提出的反例不成立。Nielsen逐行审查了OpenAI公开的37000行Lean 4代码，指出两条互相独立的失败路径，并写成Lean代码在Lean 4.32.2下编译验证。

核心信息

Connes刚性猜想是什么

数学上可以给一个群配上代数结构，有时两个不同构的群会生成完全相同的代数结构。Connes在1980年左右提出猜测：只要群满足两个附加条件——ICC条件和Kazhdan性质(T)——就不会发生这种情况。要反驳该猜想，需要构造出同时满足两个条件但生成代数结构相同的群。

AI的构造与Nielsen的反驳

OpenAI新模型构造了两个不同构的群，声称它们生成同样的代数，并附有满足ICC和性质(T)的证明。整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过。

Nielsen指出，AI构造的其中一个群实际上既不满足ICC，也不具有性质(T)，可能原因有三种：

1. 代码中的性质(T)未忠实对应Kazhdan原始定义；
2. 代码中的群与说明文档描述不一致。

Nielsen将整合后的代码中每个数学对象与行号对应，例如零上闭链群在第13700行，扭曲群在第14069行，代数同构证明在第36712行，主定理在第36954行。她追查了ICC证明的整条推理链（第31430行至第31610行），发现相关引理处理的是经对偶变换后的对象，而非原群本身，未覆盖关键元素。

Nielsen表示，对于另一个扭曲的群，她未独立核实其ICC属性，但即便它满足条件，也不改变整体结论——因为已经有一个群不满足条件。

形式化验证的局限

Nielsen在论文最后一节指出，Lean内核只能保证证明在形式上严谨，不负责证明内容是否与原始猜想意图一致。陶哲轩对此有类似说法：验证证明的是形式陈述本身，而非陈述与意图的相符性。

此前已有类似案例：一份针对五个常用Lean基准的审计发现了4833条通过机器验证的问题，包括反例、空洞定理和不可靠公理，最终由人类构造反例才揭示被证明的陈述本身是错误的。统计学习理论中这类问题被描述为“对错误陈述的成功证明”。

值得关注

Nielsen的结论是：OpenAI的形式化证明可能每条结论都正确建立，但这些结论与猜想的原话是否相关，是Lean内核无法检查的。Connes刚性猜想目前仍处于开放状态。

论文地址：https://philarchive.org/archive/NIEWTCv17
参考链接：https://openai.com/index/ten-advances-in-mathematics/ 及 https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean