7.7
深览指数
科技量子位·梦晨··AI 生成
数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”
OpenAI 宣称其下一代 AI 模型推翻了 Connes 刚性猜想，但次日数学家 J. L. Nielsen 发表论文，指出 AI 构造的反例中有一个群不满足前提条件（ICC 和性质(T)），因此该反例无效。Nielsen 逐行审查了 37000 行 Lean 代码，发现 AI 证明的是形式正确的陈述，而非原猜想本身。本文揭示了 AI 在数学证明中的核心局限：机器验证的是形式一致性，而非与人类意图的对应关系，人类审查不可替代。适合对 AI 数学能力、形式化验证及科学哲学感兴趣的读者。原文 ↗
核心观点
- ▍OpenAI 声称 AI 推翻 Connes 刚性猜想的反例不成立，因为 AI 构造的其中一个群实际不满足前提条件（ICC 和 Kazhdan 性质(T)），反例无效。
- ▍AI 证明通过 Lean 形式验证，但验证的是形式陈述本身，而非该陈述是否对应原猜想意图，因此人类审查仍然关键。
- 01数学家 J. L. Nielsen 逐行审查了 OpenAI 公开的 37000 行 Lean 4 代码，列出每个数学对象的新代码名和行号，发现关于 ICC 性质的证明链处理的是对偶变换后的对象，未覆盖关键元素。
- 02Nielsen 指出 AI 证明存在三种可能错误：代码中性质(T)未忠实对应 Kazhdan 原始定义；证明只对部分成立却被算到整个群；代码中的群并非说明文档描述的样子。
- 03过去审计发现，针对五个常用 Lean 基准的审计中，有 4833 条通过机器验证的发现（包括反例、空洞定理、不可靠公理）被人类用构造反例的方式证明为错误。
- 04安全风险在统计学习理论中被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。
反方 / 局限
- — Nielsen 承认自己未从代码独立核实另一个扭曲的群是否满足 ICC，代码中的引理可能确实证明了它满足，但这不影响结论——已有一个群不满足前提。
- — 即便 AI 证明有误，其构造方法和 Lean 形式化流程仍可能启发部分数学思考，但本文未深入探讨这种潜在价值。
6 分钟 · 4 卡片 · 11 资料
读原文 →