openai声称其最新一代ai模型成功攻克了10项世界级数学难题,其中一项便是推翻了connes刚性猜想。
次日,一篇由人类学者撰写的论文迅速作出回应:AI所提出的反例并不成立。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜

作者为堪萨斯大学拓扑物理中心的J. L. Nielsen。他逐行审阅了OpenAI公开发布的37000行Lean 4代码,将每个形式化对象精准映射回其原始数学定义,最终指出两条彼此独立的失效路径。

具体证明细节对非专业人士而言极为艰深,就让AI与数学家在专业领域内交锋吧。
但此事清晰表明:人类对AI产出科研成果的审查环节,依然不可或缺。

Connes刚性猜想是什么?
该猜想关注的是群与其关联冯·诺依曼代数之间的唯一性关系。
数学中,可为任意群赋予一个特定的算子代数结构。现实中存在两个明显不同构的群,却生成完全相同的代数对象。
Connes于上世纪80年代初提出一个断言:若某群同时满足两个额外条件,则这种“结构相同但群不同”的现象不可能出现——代数结构唯一决定了群本身。
这两个关键条件分别是:ICC(无限共轭类)性质与Kazhdan性质(T)。
换言之,要证伪该猜想,必须构造出两个非同构的群,它们均满足ICC和性质(T),却导出相同的冯·诺依曼代数。
OpenAI新模型的做法正是如此:它构建了两个不同构的群,并声称二者均具备上述两性质,且生成同构代数;整套论证以37000行Lean 4代码实现,经Lean内核实例验证通过,并附有详细构造说明文档。

Nielsen指出:AI所构造的其中一个群,实际上并未满足任一附加条件——既不具备ICC性质,也不具备Kazhdan性质(T)。

造成这一偏差的原因可能有三:
- Lean代码中对性质(T)的形式化定义未能准确反映Kazhdan原始定义;
- 所给出的证明仅适用于局部子结构,却被错误推广至整个群;
- 或者代码中实际操作的对象,与说明文档描述的群并非同一数学实体。
37000行代码,逐行溯源
为确证上述判断,Nielsen完成了一项极其繁琐的工作。
公开版本代码已被合并为单一文件,早期模块化开发阶段使用的变量名、结构名等全部消失。
为此,他编制了一份详尽对照表,将每个核心数学对象在当前代码中的标识符及其所在行号一一对应标注:
零上闭链群位于第13700行,扭曲群出现在第14069行,两套代数同构性的证明见于第36712行,主定理陈述则在第36954行。
他还完整追踪了代码中关于ICC性质的全部推理链条:起点为第31430行,逐层向上归约,最终结论合成于第31610行。

Nielsen指出的关键问题在于:这些引理所作用的对象,是经过对偶变换后的新结构,而非原始含中心元素的群本身。因此,相关推理并未覆盖到判定ICC所必需的核心部分。
至于这些中间结论能否真正传导至最终定理所涉及的具体群实例,取决于两套构造之间接口的设计是否严密。
这意味着问题本质并非“证明过程是否正确”,而是“所证命题是否就是原猜想所要求的内容”。而Lean仅能保障前者的逻辑严密性。
对于另一个被扭曲构造的群,Nielsen持审慎态度。他表示尚未独立复现代码中关于其ICC性质的验证,也承认其中某些引理或许确实成立;但这不影响整体结论——只要一个条件不满足,反例即告失败。
他将自己提出的两条反驳路径同样编写为Lean代码,并在Lean 4.32.2环境中成功编译运行。
机器验证的是语法,不是语义
论文末节将此次事件置于更广阔的理论背景下加以讨论。
Lean内核所能担保的,仅是一段形式化证明在其自身逻辑系统内无矛盾、推导链条完整;但它无法判断该证明是否真正回应了原始数学问题的实质含义。
这里可直接援引陶哲轩的观点:形式验证针对的是命题本身的句法正确性,而非其与人类意图的一致性,因此人类专家的介入不可替代。
类似案例此前已有先例。
一项面向五个主流Lean基准库的全面审计共发现4833处隐患,涵盖反例误判、空洞定理、依赖不可靠公理等问题——所有这些都顺利通过了机器验证。最终仍是依靠人类研究者构造出真实反例,才揭示出已被“证明”的命题本身即为假命题。

在统计学习理论的形式化工作中,“最危险的情形”被明确定义为:“不是一次失败的证明,而是一次对错误命题的成功证明”。
张量网络领域的研究也曾记录同类现象:系统输出的证明在形式上完全合规,只是其所证命题比预期目标显著削弱。
Nielsen强调,OpenAI提交的这份形式化工作,很可能在其内部逻辑框架下,每一条推论都是严格成立的。但它未能建立、且Lean也无法检验的,是这些推论与Connes刚性猜想原始表述之间是否存在有效关联。
人类阅读猜想时会自然识别前提条件;而证明助手面对一个不满足前提的数学对象,仍会忠实地验证关于它的任何衍生断言。
Connes刚性猜想至今仍未解决。
论文地址:
https://www.php.cn/link/3813c4c230c66feb65ebacb4b6391cdc
参考链接:
[1] https://www.php.cn/link/3aff21f3c5ef07dc5335413b767ff0cc
[2] https://www.php.cn/link/86cd7e17b9c8ca843473971b91a6fb99
本文源自微信公众号“量子位”,作者:梦晨,36氪经授权发布。











