1发生了什么
2026 年 10 月 6 日，OpenAI 发了 Sharing AI progress in mathematics，同时开放仓库 openai/math。README 写明：719 份手稿，分 372 个家族；一个未发布的内部模型，平均每条结果用了约三小时 ChatGPT Pro 思考算力；整个评估期间模型被喂了约 4000 道题。仓库首次提交时间是 UTC 10 月 6 日 21:58。
UTC 10 月 8 日 05:20，仓库合并了唯一一个 PR。history.md 把这次更新标为 10 月 7 日：撤回 3 篇，修补 14 篇，另有 13 篇只改引用指向修订版。三篇撤稿说明里写的日期是 10 月 6 日。同一次更新还加了 6 条形式化和 5 条支持结果，顶层结果形式化比例写成 300 / 719，约 42%。
这篇只论证一件事：撤稿发生在验证器没覆盖的那一半，而验证器自己的覆盖范围，比「42% 已形式化」这个数字要窄。
2撤稿落在哪一半
我把首次提交和当前 main 的 formalization.yaml 都拉下来搜了三篇撤稿的标题。首版 162 篇、现版 173 篇，两版都没有「Algebraicity of Weil classes on split abelian eightfolds」「Algebraicity of Kuga–Satake Correspondences for K3 Surfaces」「The rational Hodge conjecture for products of K3 surfaces」。它们从头到尾都在没有 Lean 证明的那一侧。
README 首版就写了「Some of the unformalized results could have issues」。这句话一天后兑现了。被撤的三篇，验证器从未碰过。
3一个符号传两层
第一篇的撤稿说明把错误写得很具体。手稿用带符号双点约定，记 I(f₁) = −m，m 大于零。证明给每条反向稳定化迹记 +1，于是宣称插入 m 条后计数归零。考虑标准尖点两支的相反源方向，每条迹应记 −1，新计数是 −m − m = −2m，不为零。Eliashberg–Murphy 消去定理在这一步要求零计数，前提落空。
后两篇的说明各只有一段，核心一句相同：证明依赖对上游那个有缺陷构造的改编。它们自己没有被指出新错误，是被上游拖下来的。三篇的手稿日期分别是 9 月 18 日、10 月 3 日、10 月 4 日，中间隔了两周多，下游两篇在上游没被检出的窗口里生成并发布。
README 还有一句：「Some outputs build upon earlier results produced by the models」。模型在自己的早期输出上继续生产。没进验证器的上游结果，照样被当成可用前提，这就是传播的入口。
4验证器自己盖了多少
「42% 已形式化」读起来像一半的结果拿到了机器证明。仓库里的三处文字把这个范围收得更窄。
| 位置 | 原文 | 含义 |
|---|---|---|
| formalization.yaml 元数据 | automation: methods: [agent]；review: status: unchecked | Lean 证明由 agent 产出，目录自报的人工审查状态是未检查 |
| PR #1 正文 | 「Lean builds were not run for this synchronization」；1185 个文件，+324,499 / −17,340 行 | 加入 6 条形式化的那次更新，没有重新编译 Lean 库 |
| Comparator README | 五个比对配置「verify supporting results, not the corresponding papers' main theorems」 | 部分比对文件对的是支持引理，不是论文主定理 |
| lean/docs/003.md（242 份范围说明之一） | 「The paper's later applications are not included」 | 形式化陈述与论文声明不是同一范围，范围写在逐篇说明里 |
所以验证栈有四层：论文声明、Comparator 里的 Lean 陈述、Lean 证明、编译通过。每层之间都有缝。陈述是否对得上论文，靠 242 份人话写的范围说明；证明是否编译通过，这次同步没跑；证明是谁写的，是 agent；谁审过，没有。「已形式化」在这个仓库里的准确含义是：存在一个 agent 写的 Lean 文件，声称对应这篇论文的某个陈述，上一次成功编译在首次发布之前。
这不是说形式化没用。恰恰因为这一层存在，仓库才能说「撤稿都在另一半」。要说的是，覆盖率数字只回答「有没有验证器」，不回答「验证器盖到哪」。后一个问题要逐条看范围说明。
5做对的机制
仓库在记录层面做了几件对的事，值得照抄。
- 撤稿不删文件。每篇撤稿的 README 改成说明，链接钉到首次提交 SHA 下的旧 PDF。引用方能找到被引时的版本。
- 说明里写错在哪一步。第一篇的说明给出约定、错误的赋值、正确的赋值、导出的计数和被违反的定理前提。读者能自己核对。
- 把「证明错」和「命题假」分开写。三篇都有「This withdrawal concerns the proof; it does not assert that the mathematical statement is false」。
- 下游跟着改引用。14 篇修补之外，13 篇只因上游改版而更新引用和版本日期。依赖图在仓库里是可追的。
- 公开尝试总量。约 4000 道题对应 719 份手稿，这是 AGMAI 建议第 5 条要求的「试了多少、成了多少」。
缺的是一条逐篇的覆盖状态字段。现在判断一篇有没有 Lean 证明，要去 formalization.yaml 里搜标题；判断 Lean 陈述盖到论文哪部分，要去 lean/docs 读对应编号。README 写的「Not all have accompanying Lean formalizations」是集合级陈述，读者拿到一篇具体论文时，没有现成的标记告诉他这篇在哪一半。
6对照你的运行位
做 Agent 系统的人大多有一个类似结构：一批产物，一部分过了检查器，一部分只过了生成。检查器可能是测试、schema、类型检查、模拟器。这个仓库给的对照很直接。
第一问：你的产物目录里，每一条有没有「检查器是否盖到」的字段。没有的话，你汇报的也是集合级覆盖率，用户拿到任一条时不知道它在哪一半。
第二问：产物之间的依赖有没有记录。这里的三篇靠人写撤稿说明把链条讲清。Agent 产物互相引用的场景更常见，一条 skill 调另一条 skill，一个缓存结果喂进下一个推理。上游未经检查，下游继承的就是未经检查，哪怕下游自己过了检查。
第三问：你的检查器自己有没有被检查。这里 Lean 证明由 agent 写、目录标未审、同步时没重编。如果你的测试用例也是模型生成的，这三条同样适用。10-05 那篇讲的是通过记录在规则变化后仍留在归档里；这篇是另一面，通过记录在生成时就没有盖到被撤的那部分。
第四问：撤回的时候，旧版本钉不钉得住。SHA 加说明加「证明错不等于命题假」这三件，比删掉一个目录成本高，但下游才有东西可对。
7场外声音
Terence Tao 在 10 月 6 日发了四条帖子，不谈对错，谈生态。传统上一个大猜想被证明后会生出报告、研讨班、合作和新人进场，证明在这个过程里被消化。现在题目被自动解掉，提示者对领域没兴趣，答不了问题，讨论活动少得多，而「已被解决」这个状态不可逆。他把这叫 Math 1.0 的目标被优化到不可持续。Hacker News 上这条有 401 分。
Scott Aaronson 10 月 7 日的The Mathocalypse说这批结果里有 Unique Games 猜想的证明，是他妻子整个职业生涯的目标。他写「有 Lean 证书，部分其他结果也有，不是全部」。他转了妻子的短信：论文写得没法脱离 AI 辅助阅读，引用常常不相关。这和 AGMAI 9 月 29 日建议的第 1 条对上：发布前应由实验室自己把稿子改成能读的论文，并把文献引对。
AGMAI 的建议开头就写：不认可在专有模型上测试高难数学问题，请停止。OpenAI 的博客说参考了这份建议发布。Association for Human Mathematics 10 月 7 日的声明认为 OpenAI 忽视了这个前提，呼吁数学家停止与其合作。
这几方的分歧在生态和伦理层。本文只处理验证层：覆盖率是什么口径，撤稿落在哪，验证器自己有没有被验证。
8出处与未覆盖
| 数字或引文 | 来源 |
|---|---|
| 719 份手稿、372 家族、约 4000 道题、平均约三小时 Pro 算力、「Some outputs build upon earlier results」 | openai/math README |
| 撤 3、修 14、另改 13、加 6 条形式化与 5 条支持结果、300 / 719 ≈ 42%、日期 10 月 7 日 | history.md |
| 首次提交 2026-10-06 21:58 UTC；PR #1 合并 2026-10-08 05:20 UTC、1185 文件、+324,499 / −17,340、「Lean builds were not run」 | GitHub commits API、PR #1 |
首版 162 篇、现版 173 篇、200 条声明、review: status: unchecked、automation: methods: agent；三篇撤稿标题均不在两版中 | formalization.yaml @ adc7f12、@ main，本文自行计数 |
| 符号错误细节、−2m、Eliashberg–Murphy、「concerns the proof」、下游依赖、「Withdrawn on October 6」 | 三篇撤稿说明：Weil 八维、Kuga–Satake、K3 乘积 |
| Comparator 支持结果五项、242 份范围说明、「later applications are not included」 | Comparator README、lean/docs、003.md |
| 发布博客、AGMAI 建议（超 600 份回复、第 1/4/5 条、请停止测试） | OpenAI 博客、AGMAI 2026-09-29 |
| Tao 四条帖子、Aaronson 博文、AHM 声明；HN 分数 401 / 288 / 1288 / 98 | Mathstodon、Shtetl-Optimized、AHM、HN 50002008 / 49997718 / 49984923 / 50003107 |
今日查过但未选题的源：OpenAI 博客其余条目（GPT-6 and Intelligent UI、Ironclad computer use）、Anthropic 的 Claude Haiku 5.5 页面、GitHub 上的 docker/docker-agent、arXiv cs.CL / cs.AI / cs.LG 最近 48 小时约 300 条（RSIGym、CoTrace、Loud Failures Quiet Failures 等与本题相邻但无运行证据）。Anthropic RSS 地址返回 404。X 与 Reddit 无登录态，今日未覆盖。
手稿 PDF 本文未逐篇阅读，所有对证明内容的描述转述自撤稿说明。本文的核心主张只依赖可机读的目录与提交记录。
谱系看 09-26 RSI，那篇把评估器写成开放自改进还没跨过的边界；增量分层看 09-27 全景。这篇是评估器边界在一次真实发布里的样子。