10 月 6 日，OpenAI 在 GitHub 上一次性放出 722 份数学手稿，说它们覆盖了 372 个数学开放问题。 相关标题很快铺满时间线。第二天，三篇关于霍奇猜想的论文因符号错误被撤回。 而更早的纳维-斯托克斯方程证明，虽然“已通过 Lean 验证”，也被发现和形式化代码对不上。知乎微博
同一件事于是有了两种读法：一边说 AI 改写了数学，一边说这批东西是“数学泔水”。普通人真正该弄清楚的，不是谁对谁错，而是“验证”到底验到了哪一步。
Lean 是证明检查器。它逐行检查代码里的逻辑，但检查的是代码里的那句话，不是你原本想证明的那句话。剑桥和伦敦国王学院的研究者把 OpenAI 的 NS 手稿和 Lean 代码逐段对照，发现一处关键条件对不上：论文说某个估计只需额外 4 阶导数，代码用的却是 5 阶。 条件更强，证的其实是一个更弱的命题。像翻译软件把“这句话”翻成“另一句话”，语法全对，意思变了。知乎
这不是孤例。据一份统计，722 篇里只有 162 篇附了 Lean 形式化，模型和提示词也没公开。 把思维过程放出来的只有 10 篇。 大多数手稿停在同一个位置：公司说它解了，独立复核还没跟上。微博知乎
这不等于结果都是假的。不少数学家承认，其中一些证明很可能是对的，甚至相当漂亮。问题在于“对”和“可验证”之间还有距离。有人分析那 700 多篇手稿，发现很多证明是同一套路：把式子展开到很高的阶，让高阶余项在某一刻精确抵消。 这通常说明背后有真实结构，但模型没把结构提炼出来，只是用算力把路硬算通了。答案有了，理解没有。知乎
最新的几批成果把问题推得更远。10 月 26 日，OpenAI 说模型证伪了指数时间猜想（ETH），并给出 Lean 证明。这次比 10 月 6 日谨慎：请 ETH 的两位提出者 Impagliazzo、Paturi 和 MIT 的 Ryan Williams 组织独立审查。但三人说得很清楚：参与审查不等于为结论背书。 截至 10 月 28 日，审查仍在进行。知乎
同一批手稿里，也有人声称“局部平滑猜想被推平”。有人逐条核对 079 号手稿后指出，它证明的是三维欧氏空间半波方程的特定版本，不是所有维度的局部平滑猜想。 论文有边界，标题没有。知乎
把这几件事放在一起，普通人只需问四个问题：这是谁说的，Lean 验的是哪一句话，那句话和原命题是不是一回事，有没有独立的人读懂并愿意负责。四关都过，才叫“验证通过”。只过第一关是“宣称”，过第二关是“代码通过”，过第三关才谈得上“数学上成立”，过第四关才是共同体接受的知识。
这套区分不只适用于数学。AI 让“给出答案”变便宜，让“确认答案”变昂贵。722 篇手稿是一次预演：当生成速度超过验证速度，知识的瓶颈就从“想出来”移到“查清楚”。陶哲轩把它叫“证明消化不良”。 MIT 的 Henry Cohn 说得更直白：这些证明在制造“技术债务”，正确但难读，像“数学泔水”。 他们担心的不只是 AI 取代数学家，而是答案像洪水涌来后，谁来为理解买单。微博知乎
奥尔特曼在 10 月 30 日的播客里说，他理解数学家的处境，但 OpenAI 不会停止发布；人类有权了解宇宙的基本规律。他承认发布方式需要改进，也说 OpenAI 在数学上投入了数亿美元，单是 NS 方程就花了约 1000 万美元。 这话很宏大，却绕开了一个小问题：“有权知道”和“有能力核实”不是一回事。把 722 份大多未经独立复核的手稿放在网上，不等于把知识交给人类；它更像是把核查成本转手交给了数学界。微博
所以普通人该怎么看？不必把 AI 当神，也不必把它当骗子。不妨把它当成一个产量惊人、但还没学会“把话说清楚”的合作者：它给出的东西，先当线索，别当结论。真正值得盯的，不是它又解了几道题，而是有没有人能把那些证明读懂、简化、讲明白。数学的价值不只在答案，也在一条别人能走的路。AI 可以先把路修到山顶；但在另一个人独立走上去之前，那还不算路。
