OpenAI 的 math 仓库里，现在躺着 719 篇数学手稿，归在 372 个成果族里。更扎眼的数字不是 719，而是 3。

仓库刚上线没几天，3 篇论文已经因为一个符号错误被撤回，另有 14 篇被修补，13 篇跟着更新引用关系。

很多人的第一反应大概是，AI 证明果然靠不住。也有人已经急着把它讲成数学界的 AlphaGo 时刻。我觉得这两种读法都太快了。

我把这个仓库完整拉了下来。它有 3.2GB，里面有 776 个 PDF、12 万多个 Lean 文件。README 写得相当克制，719 篇论文并不是同一个置信等级，约 42% 的顶层结果有 Lean formalization，其余内容仍可能有问题。

这份诚实，比 719 这个数字更有价值。

因为它把一个开发者一直在回避的问题摆到桌面上。模型产出越来越快以后，我们怎么区分「看起来很厉害」和「可以进入生产」？

数学是一个极端场景，却刚好给 Agent 工程上了一课。以后真正稀缺的，未必是生成答案的模型，而是能把答案变成可检查工件的系统。

719 不是 719 个已经结案的事实

先把热闹压下来一点。

OpenAI 在 README 里明确写了，这批材料由未发布的内部模型产出，主要用于开放数学问题的评测。大约向模型提出了 4000 道问题，再按成果的重要性、依赖关系和主题聚合成 372 个族、719 篇手稿。平均每个结果使用约 3 小时 ChatGPT Pro 级别的 thinking compute。

这里有三个容易被新闻标题抹平的层次。

第一层是「模型给出了一个候选论证」。这已经很强，但候选论证离数学共同体承认的定理还有距离。

第二层是「候选论证被写成可读的手稿」。仓库里的 PDF、源码、引用和构建说明都属于这一层。它让同行可以阅读、质疑和复现，不等于同行已经认可。

第三层才是「论证被机器形式化检查」。OpenAI 放出了 Lean library 与 formalization catalogue，并给了 comparator instructions。也就是说，部分结论不是让读者凭感觉相信，而是让 proof assistant 编译验证。

这三层不能混在一起。

如果一篇文章只写「AI 解决了多少未解难题」，那是在用第三层的确定性感染第一层。真正严谨的说法应该是，模型生成了一大批高价值的候选研究成果，其中一部分已经进入形式化验证，其余仍在公开审查的路上。

这不是咬文嚼字。数学对「成立」的定义本来就严苛，软件工程也该有同样的脾气。

三篇撤稿，反而是这次发布里最重要的部分

10 月 7 日的 history 文件记录了一件很不讨喜、也很关键的事。

「Algebraicity of Weil classes on split abelian eightfolds」里发现了一个 sign error。这个错误让一个 stabilization-trace cancellation argument 失效，连带使两篇依赖它的论文一起撤回。仓库没有偷偷把 PDF 替换掉，而是在历史页说明了缺口，并保留被撤材料的指向。

3 篇撤回。14 篇修复。13 篇更新依赖引用。

这串数字看起来不够传奇，却很像真正的工程。

写过 Java 或 Spring 服务的人应该很熟悉这个画面。一个底层公共组件的符号处理错了，最先爆的不是组件本身，而是上层几个看起来完全无关的接口。你不能只修那一行，还得找依赖图，跑回归，检查哪些服务把错误结果当成前提继续推下去了。

数学论文的引用网络和微服务依赖图，没那么遥远。

一篇手稿的错误如果被当成前提，后续手稿的正确性就不再是单点问题。这次仓库把这种影响面显式留下来，倒让我对它多了一点信任。不是因为它没有错，而是因为它把错误当成版本系统里的事件，而不是公关事故。

很多团队做 Agent 项目时反而走向另一个方向。演示录像里 Agent 自动调工具、写代码、发 PR，一路绿灯。失败的 trace 被丢掉，人工兜底没有记录，测试环境的偶然性也没有说明。发布时大家只剩一句「它完成了任务」。

可你无法审计一个被剪辑过的成功。

数学仓库至少做了更对的一件事，给结果附上版本、依赖和撤回记录。它没有消灭不确定性，只是把不确定性放到了台面上。

Lean 不负责让模型更聪明，它负责让错误没地方躲

有些讨论把 Lean 看成给 AI 贴金的认证章。这个理解不太对。

Lean 不是说模型的思考过程很优美，也不判断这个定理有没有科研价值。它只做一件事，检查你写下的形式化命题，能不能从已接受的规则一步一步推出。

这件事听着朴素，落到现实里却很硬。

自然语言里的「显然」「类似地」「由前引理可得」，经常藏着省略的前提、变量范围变化，或者一个没被注意到的符号方向。人读论文时会靠经验补全，偶尔也会跟着误读。proof assistant 不会替你补。

模型写出一段漂亮推理，和模型给出 Lean 可以通过的证明，不是同一种能力。前者在生成，后者在接受约束。

OpenAI 这次的顶层形式化比例大约为 300/719。这个比例本身也提醒我们，形式化验证并不便宜。数学家需要把自然语言论证翻译成精确对象、引入库中已有的定义、补完全部引理，再让编译器检查。它更像把一份口头需求做成一组可执行规格，不像点一下「验证」就会出绿勾。

我自己的判断是，42% 不是一个可以拿来庆祝的完成率，也不是一个可以嘲笑的低数字。它是一个很真实的边界。生成可以快得惊人，验证仍然是慢工，而且必须由系统化的流程来接住。

这恰好是 Agent 从玩具走到生产时最缺的部分。

对 Agent 来说，答案不是交付物，可验证的副产物才是

把数学换成日常开发，逻辑就清楚多了。

假设你让一个 Coding Agent 完成「给订单服务加退款接口」。它最终给出一段代码和一句「测试已通过」。如果交付到这里，你拿到的仍然只是一个自然语言承诺。

更可靠的交付物至少应该包括这些东西。

  • 改动的 diff，能看清它碰了哪些边界
  • 可重复执行的测试命令和测试结果
  • 数据库 migration 与回滚方案
  • API contract 的变化
  • 依赖版本和构建日志
  • 失败过的尝试，尤其是它为什么放弃某个方案
  • 对风险点的声明，例如幂等、并发退款、权限与审计

这套东西听着像流程负担，实际上是给未来的你留证据。

Agent 生成速度越快，证据链越不能省。人类 review 的注意力是有限的，最危险的不是 Agent 写错一行代码，而是它写了五百行看似合理的代码，你没有任何入口判断应该从哪里怀疑。

数学里的 Lean proof，工程里不一定非得是 formal methods。对 Java/Spring 团队而言，它可以是 contract test、property-based test、数据库约束、静态分析、权限回归、可回放的 trace。关键不是工具名字，而是把「我认为它对」转换为「系统可以独立检查它在什么范围内对」。

这话听着有点刺耳，但只要 Agent 还会幻觉、会误解仓库约定、会把临时成功当成稳定成功，测试和约束就不是收尾工序，而是 Agent 系统的一部分。

别只盯着 Agent 的推理，先设计它能留下什么证据

很多 Agent 架构图画得很漂亮。Planner 拆任务，Executor 调工具，Reviewer 回看结果，Memory 记录经验。可真正跑到复杂任务时，最容易被遗漏的一层是 Evidence。

我更愿意把一个能进生产的 Agent 看成四段链路。

1
2
3
4
任务意图
  -> 可执行计划
  -> 工具调用与中间工件
  -> 独立验证与可追溯记录

最后一段不能只是另一个 LLM 说「看起来不错」。模型自审有用，但它不是独立验证。就像让同一个人既写单测又签字批准上线，效率很高，约束很弱。

更实用的做法，是在每类任务前就定义验收器。

对于代码修改，验收器是编译、测试、lint、依赖扫描和 diff policy。对于知识问答，验收器是可定位的原始来源、引用片段和时间戳。对于订单、支付、发帖这类动作，验收器还要包含权限范围、审批点、幂等键和外部系统回执。

LangGraph 这类框架擅长编排节点，但图里应该有一类不讨喜的节点，专门做 validator。它不负责把话说得好听，只负责拒绝不满足条件的结果。

例如一个发布文章的 Agent，不能以「生成 markdown 完成」为结束。它要跑 frontmatter 校验、检查链接、确认 git status 只有本次变更、执行构建，并保存部署返回的 URL。任何一步失败，状态都应停在可恢复的位置，而不是由模型用一段安慰性的总结把失败盖过去。

这就是数学仓库给工程师的真正提示。质量不是一个分数，而是一条能回看的链。

可解释和可验证，别混成一件事

这次还有一个很容易被忽略的反差。

一方面，OpenAI 放出了 reasoning summaries。另一方面，它没有把这些摘要当成证明本身，而是同时给出手稿、形式化材料和检查说明。

原因很简单。一个过程讲得通，不代表结果已经被验证。

这对做 AI 产品的人尤其重要。用户往往喜欢看到 Agent 的思考摘要，因为它会带来一种「我知道它为什么这么做」的安全感。但摘要可能被压缩、改写，甚至只是对行动的事后叙述。它适合帮助人理解，不适合单独承担审计责任。

真正该被保存的是输入、工具参数、返回值、文件 hash、执行日志、版本号和验收结果。这些东西不优雅，阅读体验也不如一段流畅的 reasoning，但它们能在事故发生后告诉你，系统究竟做了什么。

你想想看，线上退款错了 20 笔，最需要的不是 Agent 写了一段多有逻辑的解释，而是能定位到哪次调用用了哪一个幂等键、哪次重试跨过了什么边界。

解释服务于理解。证据服务于追责和修复。

两者都要有，不能互相替代。

这批手稿也提醒我们，公开不是验证的终点

把 719 篇材料一次性公开，当然会给同行带来压力。数学家没有义务替一家 AI 公司完成审稿。对某些高度专业的领域来说，读完一篇长证明都需要不少时间，更别提检查数百篇彼此依赖的论文。

这个处境完全合理。

开源项目也有同样的问题。一个 Agent 一夜之间提 500 个 PR，不是在帮 maintainer 节省时间，除非它同时提供了足够好的分批、测试、依赖图、失败说明与回滚路径。否则只是把生成成本转嫁成 review 成本。

OpenAI 的仓库至少给了 family、目录、版本历史和部分 formalization，这是可审查性的开始。可它不是终点。未形式化的手稿仍要经历同行阅读、反例寻找、独立复现和长期引用。即使通过 Lean 的部分，也仍要确认形式化的命题是不是研究者真正关心的原命题。

形式化保证的是「代码表达的命题可推出」，不是自动保证「代码表达的命题就是你本来想说的那句话」。

这也是为什么我不太喜欢把 verification 当成一个按钮。它是一套把模糊目标逐步收紧的工程能力。

明天就能用上的一份 Agent 验收清单

如果你正在做 AI Agent，不用等到上 formal proof 才开始改变。下面这份清单已经能挡住很多看起来成功的假象。

先定义不可协商的结果

在 prompt 前写清楚哪些是必须可检查的。例如「修改必须通过指定测试」「不能访问生产数据」「只能提交到 feature branch」「外部操作必须返回 receipt」。别只写「帮我完成任务」。

把成功条件交给非模型系统

让 CI、schema、policy engine、sandbox、数据库约束或第三方 API 回执做最终裁判。LLM 可以计划，也可以生成修复建议，但不能单独宣布自己成功。

保存最小可复现包

每次重要任务至少留下任务版本、模型与 prompt 版本、工具调用序列、输入输出摘要、产生的文件和验证结果。出问题时能重放，比事后追问模型靠谱得多。

让失败成为一等公民

记录失败不是为了找模型难看。它会告诉你验收器缺了什么、工具权限是否过宽、任务拆分是否太粗。OpenAI 撤回三篇手稿的做法就值得借鉴，保留事件和影响范围，而不是假装它没发生过。

把人工 review 用在模型最不擅长的地方

人不应该逐行重复机器已经能做的检查。人该看需求有没有被正确翻译、约束有没有漏、异常路径会伤到谁、结论是否值得承担后果。把确定性检查自动化，人才能把注意力留给判断。

从一处符号错误，回到我们每天写的代码

数学证明里的一个 sign error，可以撤掉三篇论文。业务代码里一个负号、一次错误的重试、一个过宽的权限，也可以让三个月后的账目对不上。

区别只是数学家会把它叫作证明缺口，工程师会在凌晨看到告警。

OpenAI 这次放出来的 719 篇手稿，最大的价值不在于我们今天能不能读懂每一个定理。它让人看见，生成能力冲到前面时，验证、版本和责任链会立刻成为瓶颈。

对开发者而言，别把 Agent 当成一个更会说话的代码生成器。把它当作一个需要被约束、被观测、被验收的协作者。

它交出答案的那一刻，不是任务结束。

能让答案经得起检查，任务才刚刚进入正题。

参考资料