10 月 6 日OpenAI 在 GitHub 上一次性公开了 722 篇数学手稿声称在几何、代数、计算机科学等方向的 372 个问题上取得进展。第二天撤回 3 篇一个符号错误让其中一篇的论证失效另外两篇依赖了同一个构造一并作废同时修订 14 篇还改了一处过时引用。手稿总数从 722 变成 719。这批东西没走同行评审也没发在 arXiv而是直接传到自家仓库。据 OpenAI 方面对媒体的说法错误是内部审计时发现的约一半结果在发布时并未经过确认合作方 AGMAI 的建议是不必等完全形式化再发。10 月下旬陶哲轩和邓煜在一场对谈里把这类产出称作有毒废料——这话针对的不是 AI 会不会做数学而是把解数学题当基准测试这种做法。技术上看变的是发布方式AI 能不能做数学两位数学家都没否认甚至看好它在真正的研究里加速。争的是产出和验证之间的顺序被调换了。以前的路子是人有想法AI 补细节写完自己核一遍。现在的路子是AI 批量生成人来做验收。据报道这批手稿来自约 4000 次会话产出 722 篇成功率不到两成——这个比例本身不算丢人问题是剩下那八成里有多少被当成结论发了出来。生产端的边际成本接近零验证端的成本一点没降。甚至更高读一份没有思维链、引用不透明、符号还可能有错的证明比自己做一遍更累。邓煜提的两条边界说的就是这个——过去有证明的问题和人类理解的问题是同一条线现在中间裂开了一条有证明但只有 AI 知道人不懂。这跟写业务代码是一回事看着离得很远其实是同一个结构。AI 生成代码的成本已经很低低到不少团队开始用每天合入多少 PR衡量效能。但验证成本没变code review 要人看测试要人写线上出事要人背。产出量一旦成了 KPI被压缩的一定是验证环节。表现是 review 从逐行看变成扫一眼 CI 绿了就过测试从覆盖边界变成跑通主流程。账不会消失只是从开发阶段挪到了故障复盘会上。Lean 这类形式化工具本来是条出路——证明可以机器校验不依赖人的耐心。但据报道这批手稿里大量文字证明和 Lean 代码之间存在断层形式化覆盖并不完整。工具在覆盖率不够约等于没有。三个能落地的做法一、把验证做成流水线别指望自觉。类型检查、lint、单测、集成测试该卡的卡住。人一定会偷懒机器不会。二、独立复算别让模型自证。让生成答案的同一个模型去检查答案等于让它给自己判卷。能用确定性方法验的就别用概率方法验。比如下面这段fromfractionsimportFractiondefcheck(n_max50):用精确有理数复算 sum(k^3) (n(n1)/2)^2返回第一个反例。forninrange(1,n_max1):lhssum(Fraction(k)**3forkinrange(1,n1))rhsFraction(n*(n1),2)**2iflhs!rhs:returnn,lhs,rhsreturnNoneprint(check(200))# None表示 1..200 全部成立跑 1 到 200 返回 None全部通过。这不是证明只是低成本证伪——但对 AI 产出来说绝大多数错误死在这一步就够了。这里用 Fraction 而不是 float因为浮点误差既会制造假阴性也会掩盖真问题。三、留痕。记录 prompt、模型版本、生成时间、人工改动。出问题时这段到底是谁写的、怎么来的必须有答案。AI 不会背锅签字的那个人会。几个坑LLM 自评不可靠。让模型输出我已仔细检查没有任何信息量它对自己的错误没有感知能力语气却一样笃定。形式化验证有成本。写 Lean 比写自然语言证明慢得多只值得用在高价值、高风险的断言上全量上不现实。看起来对是最危险的信号。符号错误、量词顺序、隐含假设这些地方 AI 出错时读起来依然通顺而人读的时候会自动脑补缺失的一步。最后陶哲轩在那场对谈里用了个开车的比喻车确实比走路快但不是所有原本走路的路都该换成开车——有时候你就是想走一走。放到工程上也成立。生成成本趋近于零之后稀缺的东西不再是产出而是谁来验、验到什么程度、验不出来的时候敢不敢说不。你怎么看评论区聊聊。