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

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

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

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