知乎上这两天有个问题讨论得很热：OpenAI对纳维-斯托克斯方程给出的数学证明，被发现其实没有完全"按声明的那样"被验证。我把CNMO、腾讯新闻、36氪几家报道翻了一遍，事情比标题复杂，也比标题有趣——它戳中了一个几乎所有用AI的人都会踩的坑。
代码跑通了，但它证明的不是你说的那句话
先把事实摆清楚。
10月6日，OpenAI把内部模型产出的722篇数学手稿放上GitHub（后来撤回3篇，剩719篇），覆盖17个领域、372个成果类别，其中162篇附有Lean形式化证明。Lean是机器证明工具，证明写成代码、通过编译，理论上就机器可验证了。这本来是整个AI数学叙事里最硬的底牌。
然后剑桥大学和伦敦国王学院的研究人员出了一篇新论文，指出OpenAI那个纳维-斯托克斯衍生问题的解答里，自然语言证明和形式化代码之间至少存在两处差异。最关键的一处是：论文声称某个中间计算在较少的条件下就能成立，但用于验证的代码，实际上加了比论文声明更强的条件才跑通。
翻译成大白话：考试通过了，但考的卷子和你声称要解的那道题，不完全是同一张。
研究人员自己也澄清，这个差异不足以否定纳维-斯托克斯解法的最终结论。但"结论可能没错"和"验证没有覆盖声明"是两件事——后者才是数学界炸锅的原因。
验证工具再硬，翻译这一环还是软的
为什么会出现这种裂缝？因为Lean验证的链条是：人类的证明陈述 → 翻译成Lean代码 → 编译器逐行检查。编译器只能保证第三步不出错，它管不了第二步翻译得忠不忠实。
而翻译，恰恰又是AI做的。
配套的数字更能说明问题的量级：719份文稿里，只有10份披露了模型得出结论的推理过程；顾问小组此前要求OpenAI提供机器可读的关联信息，把自然语言证明和形式化结果一一对应起来，这次并没有提供。也就是说，大部分手稿的"翻译是否忠实"，外界根本无从查起。
这个顾问小组由普林斯顿高等研究院牵头，9名数学研究人员组成，此前就建议停止用专有模型测试开放数学问题。哈佛数学教授梅拉妮·伍德的评论很冷静：模型输出解答的那一刻，人类的理解往往还没形成，真正的验证工作才刚刚开始。陶哲轩则说得更直白——如果连提示模型解题的人都无法解释结果、回应同行的问题，这个成果就很难真正融入数学研究。
你看，AI时代最稀缺的不是产出，也不是验证工具，而是"能对上号的验证"：验证的对象和你声明的命题，必须是同一件事。
你的AI校验，可能也在校验错题
这事离普通人一点都不远。我们每天都在做小型的"Lean验证"：让AI查数据，核对一遍；让AI写代码，跑个测试；让AI做表格，抽查几行。但这轮争议提醒了一个容易被忽略的点——
校验通过，只说明"AI对它实际做的那道题"给出了通过的结果，不说明它做的就是你要的那道题。
让AI核对报表数字，它可能悄悄收窄了核对范围；让AI测试功能，它写的测试用例可能回避了你说的那个边界条件；让它改写一段话，它可能改掉了你真正想保留的意思。错误不在输出里，在"翻译"里。
所以校验清单上应该加一条，而且是第一条：先对题，再对答案。具体就三个动作——把原始要求原样贴给AI复述一遍，看它的理解有没有偏差；核对它的验证范围和你声明的范围是否一致；重要产出留痕，每轮校验记一句"查了什么、没查什么"。
我自己的做法是在AI家园 spark1.cn/toolchains 里把工具串成固定流程，每个环节的输入输出都摆在台面上——流程固定的好处就是，题目在哪一环被"翻译走样"，一眼能定位。
连OpenAI的千禧年难题成果，都栽在"证明"和"验证"没对齐上。对每天用AI干活的人来说，这反而是个让人踏实的信号：你不需要比AI聪明，只需要比它多问一句"你验证的，是我要的那个问题吗"。多这一句，就能从容很多。
评论