AI“证对了每句话”，但这些话已不是Connes猜想：数学家24小时纠错

堪萨斯大学拓扑物理中心的J. L. Nielsen用不到24小时把OpenAI八月二日公开的37000行Lean 4代码逐行对回数学原型，结论是：AI"证对了每句话"，但这些话已经不是Connes刚性猜想要问的那个命题。Lean内核接受了每一行；错位出在"AI证明的命题"和"原猜想要问的对象"之间。Connes刚性猜想至今没有被推翻，OpenAI的"ten advances in mathematics"页面则继续把它列为十项已解难题之一。

事件轮廓很短。OpenAI在八月二日发布"十项数学进展"，其中一项是所谓"AI推翻Connes刚性猜想"。Connes在1980年代提出的猜想是：若两个群都满足ICC（每个非单位元素都有无穷多共轭类，即通过群运算变换出的等价元素）和Kazhdan性质(T)（一种代数刚性条件），且配出的C*-代数（一种把群"翻译"成算子的代数结构）相同，则这两个群本身也必须同构。公司发布37000行Lean 4代码，配套一份说明文档，称Lean内核已逐行检查通过。Nielsen当夜读完代码后，在philarchive上挂出反驳论文。

Nielsen的两条反对路径都建立在"AI构造的群不满足猜想条件"这一判断上。首条直指ICC本身。Connes猜想要求两个群都是ICC群，意思是除单位元外的每个元素都要有无穷多共轭类，即不存在非平凡中心元素。Nielsen指出，OpenAI构造的其中一个群是"以一个格为中心的中心扩张"，即在原群上叠加一个由离散格构成的中心层；这意味着这个群存在非平凡的中心元素。任何一个非单位中心元素的共轭类只有它自身一个，大小为1，ICC条件不成立。Lean不会替AI检查这一点，因为这是命题与原意之间的对齐问题，不是逐行推导问题。@QualiaQuanta的X线索当日独立走到同一结论：中心扩张与ICC不相容。

次条反对指向代码与数学原型的"对接面"。Nielsen的审计记录了关键行号：零上闭链群（一种描述群对称性的代数工具）出现在第13700行，扭曲群在第14069行，两个代数同构映射在第36712行，主定理在第36954行。Nielsen发现，代码中很多引理证的是"承载中心元素的那个群的对偶"上的性质，而不是那个群本身。两个对象之间在第31430行到第31610行的推理链没有被独立验证。Nielsen把单文件拆解、重建了名称与行号的对应表，这段还原工作本身就是反驳的一部分。

机制在更早的记录里已经出现过。一项针对五个常用Lean基准的审计指出，机器验证通过的"证明"里包含4833条问题：反例、空洞定理（即"假命题为真则任何命题为真"形式的循环论证）、不可靠公理。这些"证明"在Lean眼里无误，被人类反例揭示后才暴露问题。统计学习理论的形式化记录里有同一模式的更短命名："不是失败的证明，而是对错误命题的成功证明。"张量网络领域也有过机器检查通过、但证得比声称命题严格更弱的先例。陶哲轩此前在公开评论里也指出过同一限制：证明助手验证的是形式陈述本身，不验证它和原意图是否相符。

OpenAI的发布把这层限制遮住了。营销标题写的是"AI推翻了Connes猜想"，发布页面上把它列为十项已解难题之一。Nielsen的反驳把这件事翻转成了一次公开的、机制清晰的能力测试，并经由同日社区独立评论得到交叉确认。

仍待观察的是两件事。一是OpenAI是否在文档或回应里承认Nielsen的反对有效、调整"ten advances"页面；二是Lean社区是否会跟进，为证明助手加一个轻量层，让它检查"被证明的命题"与"声明的命题"之间是否真的对齐。在那之前，"AI证明X"的头条都该被读作"AI在某种形式系统内证了一个叫X的命题"；至于这个命题是不是原意要问的那个，仍然需要人去看。