# OpenAI 的数学证明跑通了 Lean 检查，5 天后论文却偷偷加了 4 页

> 原标题：一份通过检查的证明，为什么在 5 天后补写了 4 页？当 AI 逼出做完的真相

- 来源：Computing Life · Share · 鸭哥调研
- 发布时间：2026-08-12T00:00:00.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/50427
- 原文：https://yage.ai/share/ai-math-acceptance-staircase-20260812.html

## 摘要

OpenAI 在 8 月 1 日发了 10 组数学成果，附带的 Lean 4 代码全部编译通过，8666 个构建任务没报错。但 5 天后，论文从 249 页涨到 253 页，作者补了一个极限情况下的推导漏洞，代码本身没改。这说明机器检查通过只代表语法和逻辑规则没毛病，不代表人类看懂了，也不代表代码真的对准了原始难题。Terence Tao 顺势提了个新...

## 推荐理由

用一个具体案例把机器验证和人类理解之间的鸿沟讲透了。OpenAI 的 Lean 4 代码全绿、Tao 的五级框架，都是硬货。没给更高分是因为这更像一篇深度评论，而不是首发爆料，但信息密度和切入角度都够扎实。

## 锐评

这条新闻讲了一个很具体的信号：OpenAI用Lean 4生成的十组数学证明，8666个构建任务一次编译通过，没报错。但五天后，论文从249页涨到253页，作者手动补了一个极限情况下的推导漏洞，代码本身没改。这说明机器检查通过只代表语法和逻辑规则没毛病，不代表人类看懂了，也不代表代码真的对准了原始难题。

文章把“做完”拆成了五级：候选生成、规则检查、意图对齐、同行理解、共同体吸收。目前十项成果里，只有一项关于非sofic群的证明走到了第五级，被后续学者直接复用；量子平行重复那项还卡在第二和第三级之间，专家坦言没消化关键步骤。Terence Tao顺势提了个新规矩：优先权不该给最早扔出代码的人，而该给最先交齐论文、解释和形式证书整套材料的团队。

正文没披露那4页补丁具体改动了哪个定理的哪个边界条件，也没给出其他五项成果为何无人审阅的细节。对AI从业者来说，这条新闻最大的提醒是：别把Agent返回的success=true当终点，测试通过和业务对齐是两码事。