OpenAI前不久刚放了个惊动科技圈和数学圈的大消息：声称下一代模型一口气拿下10个世界级数学难题，其中就包括推翻提出了40多年的Connes刚性猜想。 结果消息放出来才24小时，就被数学家实锤打脸——AI给出的证明根本站不住脚。

完成这次“光速打脸”的是堪萨斯大学拓扑物理中心的学者J. L. Nielsen，她把OpenAI公开的37000行Lean 4形式化证明代码从头到尾逐行核对，把每个代码对象对应回原本的数学定义，最终找出了两条互相独立的核心漏洞，直接判定AI提出的反例不成立。

这位学者本身横跨物理、数学、哲学多个研究领域，主攻量子引力方向，这次的反驳论文她也同步写成了可运行的Lean代码，在最新版本的证明工具上验证通过。

先搞懂：Connes刚性猜想到底说啥？

这个猜想是数学家Connes在1980年前后提出的，核心逻辑其实并不复杂：数学领域中，我们可以给一个抽象的“群”结构搭配一套冯·诺依曼代数，有时候两个看起来完全不一样的群，最终搭出来的代数结构可能完全相同。 Connes就此提出猜测：只要群满足ICC性质和Kazhdan性质(T)这两个前提条件，这种“不同群对应同代数”的情况就不可能发生——只要代数结构一致，对应的群就必然是同一个。 按照这个逻辑，想要推翻这个猜想，只需要找出两个满足这两个前提、但本身结构不同的群，证明它们对应完全一致的代数结构即可。 OpenAI当时的证明思路正是走的这个路径：构造了两个不同构的群，给出了二者都满足两个前提条件、且代数同构的证明，整套论证写成了37000多行的Lean 4代码，还通过了Lean证明助手的内核自动验证。消息刚出的时候不少人都惊叹，以为这个悬了几十年的数学难题真的被AI终结了。

但Nielsen的核查直接点出了最致命的问题：AI构造的其中一个群，根本没有满足猜想要求的两个前提——既不属于ICC群，也不具备Kazhdan性质(T)。

她分析漏洞可能来自三个层面：

  • 代码里对性质(T)的实现，没有忠实对应数学界通用的原始定义
  • 证明只覆盖了群的部分元素，结论却被错误推广到了整个群上
  • 代码里实际构建的群，和说明文档里描述的研究对象根本不是同一个

逐行“反编译”3.7万行代码：AI纯属答非所问

因为OpenAI公开的是整合成单文件的发布版本，早期开发阶段分模块时的语义化变量名、模块名全都被移除了，读起来就像一本被撕掉了目录、章节标题的厚书，根本看不出哪段代码对应哪个数学概念。 Nielsen干脆自己整理了一份完整的“代码-数学概念对照表”，把每个研究对象在代码里的位置、对应行号全部标注出来：零上闭链群在13700行，扭曲群在14069行，代数同构的证明在36712行，最终的主定理在36954行。

顺着自己整理的对照表追完整个证明逻辑链，她终于找到了问题根源：代码里关于ICC性质的所有证明，针对的都是经过对偶变换之后的数学对象，根本不是猜想讨论范围内、带有非平凡中心的原群。换句话说，这些引理本身的逻辑推演可能没有错，但它们和要证的猜想没有直接关系——证明的对象从一开始就选错了。 至于另一个被构造的扭曲群，Nielsen态度很谨慎：她表示自己没有独立从代码里核实它是否满足ICC条件，就算它真的符合要求，也改变不了整个证明不成立的结论——只要有一个群不满足前提要求，整个反例就是无效的。

【编辑观察】说直白点，这就像高考作文题让你写“新时代的青年担当”，你写了一篇文采飞扬、零错别字、逻辑满分的“我的老父亲”，每句话都挑不出错，但完全跑题了，照样拿不到高分。Lean这类证明助手就像一个只会改语法错误的阅卷老师，它根本看不出你写跑题了。

机器能查逻辑对错，却读不懂问题本身

这起“AI证明翻车”事件，刚好印证了数学家陶哲轩之前的预警：形式化证明工具能保证的，只有每一步逻辑推导在形式上严丝合缝，但它永远没法检查——你证明的这个命题，是不是你原本想要解决的那个问题。 学界早就发现过同类问题：一份针对五个主流Lean数学基准的审计，在一万多道正式题目里找出了4800多条问题，包括反例、空洞定理、不可靠公理，这些内容全部顺利通过了机器的自动验证，最后还是靠人类学者构造出反例，才发现被证明的命题本身就和预期目标不符。

统计学习理论里把这种情况列为最危险的形式化错误：最糟糕的情况不是你给正确命题写出了有漏洞的证明，而是你给一个错误的、或者偏离目标的命题，写出了逻辑完全自洽的正确证明。之前张量网络领域的AI研究也出过类似问题：系统给出的证明形式上毫无破绽，但实际证明的命题比研究目标要弱得多，根本达不到解决问题的标准。 Nielsen在论文最后总结：OpenAI的形式化代码，或许真的把它写出来的每一条小结论都证明对了，但它证明不了、Lean内核也永远检查不了的是——这些结论，到底和Connes刚性猜想的原始表述有没有关系。证明助手只会机械地验证给它的命题，不会管这个命题是不是漏掉了猜想要求的前提条件。 直到今天，Connes刚性猜想依然是一个开放的未解数学难题，并没有被AI攻克。

其实这也给当下热炒的“AI马上要替代科学家”的论调降了降温：AI确实能在形式化推演、大规模计算这类工作上给科研人员提供极大帮助，但它目前还读不懂人类提出问题时包含的所有前提、语境和边界，科研中最核心的“定义问题、校准方向”的环节，至少在现阶段，依然离不开人类学者的把关。