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_max=50):"""用精确有理数复算 sum(k^3) == (n(n+1)/2)^2，返回第一个反例。"""forninrange(1,n_max+1):lhs=sum(Fraction(k)**3forkinrange(1,n+1))rhs=Fraction(n*(n+1),2)**2iflhs!=rhs:returnn,lhs,rhsreturnNoneprint(check(200))# None，表示 1..200 全部成立跑 1 到 200 返回 None，全部通过。这不是证明，只是低成本证伪——但对 AI 产出来说，绝大多数错误死在这一步就够了。这里用 Fraction 而不是 float，因为浮点误差既会制造假阴性，也会掩盖真问题。
三、留痕。记录 prompt、模型版本、生成时间、人工改动。出问题时，"这段到底是谁写的、怎么来的"必须有答案。AI 不会背锅，签字的那个人会。
几个坑
- LLM 自评不可靠。让模型输出"我已仔细检查"没有任何信息量，它对自己的错误没有感知能力，语气却一样笃定。
- 形式化验证有成本。写 Lean 比写自然语言证明慢得多，只值得用在高价值、高风险的断言上，全量上不现实。
- "看起来对"是最危险的信号。符号错误、量词顺序、隐含假设，这些地方 AI 出错时读起来依然通顺，而人读的时候会自动脑补缺失的一步。
最后
陶哲轩在那场对谈里用了个开车的比喻：车确实比走路快，但不是所有原本走路的路都该换成开车——有时候你就是想走一走。放到工程上也成立。生成成本趋近于零之后，稀缺的东西不再是产出，而是"谁来验、验到什么程度、验不出来的时候敢不敢说不"。
你怎么看，评论区聊聊。
