OpenAI 的 Astra 被光速打脸：37000 行代码逐字验证，AI 证对了每句话但跟原题毫无关系
AI飞行客 OpenAI 的 Astra 被光速打脸：37000 行代码逐字验证，AI 证对了每句话但跟原题毫无关系
故事得从昨天说起
昨天我刚写了一篇关于 OpenAI Astra 让数学界”集体破防”的博客——2000 美元解十个数学难题，推翻 Connes 刚性猜想，一片”数学还有啥意义”的哀嚎。
然后今天的故事走向，比任何编剧写的剧本都精彩。
OpenAI 的 10 个成果中，最重磅之一的”推翻 Connes 刚性猜想”，被堪萨斯大学拓扑物理中心的一位数学家 J. L. Nielsen，在 24 小时内就用一篇人类论文驳回了。
注意，不是反驳，是驳回。数学意义上的”你错了”。
37000 行代码，逐行对号
Nielsen 干了件什么事？
OpenAI 公开发布了 Connes 刚性猜想证明的 Lean 4 代码，整整 37000 行。Nielsen 从头追到尾，把每一个数学对象对回它的原始定义。
这不是读新闻稿那种看热闹，这是真·硬核实证。
他列了一张对照表：零上闭链群在第 13700 行，扭曲群在第 14069 行，两套代数同构的证明在第 36712 行，主定理在第 36954 行。然后他沿着 ICC（群论中的一个附加条件）的推理链追了一遍——从第 31430 行起步，一路追到第 31610 行得出结论。
他发现了什么？
AI 构造的其中一个群，其实根本没有满足那两个附加条件。既不是 ICC，也没有性质(T)。
也就是说，OpenAI 证明了一个东西——但不是 Connes 刚性猜想让他们证明的东西。
这里有三层可能的问题： – 代码里性质(T)没有忠实对应 Kazhdan 的原始定义 – 证明只对部分成立，却被算到了整个群上 – 代码里的那个群，根本不是说明文档描述的那个群
机器检查的是形式，不是意思
这是整件事最有价值的一点，值得每个用 AI 搞科研的人刻在脑门上。
Lean 内核能保证的事情，只是一段证明在形式上严丝合缝。至于是不是真的证明了原结论——Lean 不负责，也负责不了。
陶哲轩早就预警过这个。一份针对五个常用 Lean 基准的审计给出了 4833 条发现，包括反例、空洞定理和不可靠公理，全都通过了机器验证。最后还是人类构造出反例，才发现被证明的那句话本身就是错的。
Nielsen 自己也把反驳写成了 Lean 代码，在 Lean 4.32.2 下编译通过。
这不讽刺吗——Human 写的 Lean 代码驳回了 AI 写的 Lean 代码。大家拿的是同一套工具，比的是谁更清楚自己要证什么。
Nielsen 在自己的论文里有一句非常精准的总结：
> OpenAI 那份形式化可能把它声称的每一条结论都建立对了。但它没有建立、Lean 内核也检查不了的，是这些结论和猜想的原话有没有关系。
翻译成人话就是：AI 写的证明都对，但它证的是另一个东西。
最危险的是”对错误陈述的成功证明”
这不是个孤立事件。在统计学习理论的形式化工作中，最危险的情形被描述为——”不是一个失败的证明，而是一个对错误陈述的成功证明”。
张量网络研究也记录过同类现象：系统给出的证明形式上完全正确，只是它证的那个命题比预期的要弱。
你现在再回头看 OpenAI 公布的”10 个成果”，细品一下这行字：
> “OpenAI 研究科学家 Noam Brown 还补了一句——我们也没在每个问题上花费太大力气”
是的，没花太大力气，所以推的对象没对上号。
这本身就说明了问题
我不是来嘲讽 OpenAI 的。说实话，能把 37000 行 Lean 4 代码跑通，这本身是个了不起的 engineering 成就。
但这件事真正应该引发的讨论不是 “AI 多牛逼” 或 “AI 被打脸” 这种流量标签——而是 AI 在数学/科研中的角色边界到底是什么？
Nielsen 做的事，本质上是一个人类数学家，在用人类的方式做 peer review：他不是在检验代码有没有 bug（虽然没有 bug 这回事在 37000 行代码里本身就存疑），他是在检验”你要证明的东西，是不是真的等于我理解的那个问题”。
这一步人类判断，目前没有任何工具能替代。
Lean 可以验证你的推理每一步都正确，但它不能告诉你——你推理的前提是不是偷换了概念。套用到更广的 AI 科研场景上：
一个 AI 可以写出一篇形式上无懈可击的论文。每个引理都正确，每个推导都合规。但如果它从一开始就理解错了研究问题——它给出的是对另一个问题的完美回答——再多的形式验证也救不了。
Connes 刚性猜想仍然是开放的。
别急着为数学”哀悼”，数学还没死
昨天我还写了《数学家的精神危机》，探讨了当 AI 能做数学时人类还能做什么。
今天的事给了一个很漂亮的答案：人类数学家的职责不是解题——是问对问题。
Nielsen 24 小时干的事，拆开来看其实很简单——一个懂数学的人坐下来，花时间把 AI 的输出跟数学的原始问题对了一遍。他发现”对不上”。
这个”对不上”，AI 自己发现不了。Lean 发现不了。37000 行全部编译通过也发现不了。
因为在数学里，最难的不是找到答案，而是确保你问的是那个正确的问题。
所以数学家们，别绝望。你们的 job security 暂时还在——只要保持一个竞争力：能比 AI 更清楚地知道自己想证明什么。