想象一下：你用一张算式证明三栋楼都站得住，后来发现其中一个正负号写反了。问题就不只是纸面不整洁。第一栋楼的承重计算失效，后两栋又建在它上面，于是三栋都得重新检查。
OpenAI这次遇到的正是这种连锁问题。它此前批量公开数学研究材料，其中部分配有Lean形式化证明——也就是把命题和推导写成机器可检查的语言。如今，OpenAI在自己的数学仓库中宣布撤回三篇手稿，原因是一篇上游手稿中的符号错误破坏了关键论证，也让另外两篇依赖它的手稿失去基础。
这里要先分清一个词：官方使用的是“manuscripts”，即手稿或预印本。撤回表示作者不再把当前版本当作有效成果主张，不等于三篇已经由期刊正式发表的论文遭到撤稿。以下错误说明、修订数量和形式化进度均来自OpenAI自己的仓库记录，目前没有材料显示这些说法已获外部数学专家独立核验。
一个负号，为什么会带倒三篇手稿？
据OpenAI仓库的更新记录，问题首先出现在《Algebraicity of Weil classes on split abelian eightfolds》中。一个符号错误使其“stabilization-trace cancellation”论证失效。
这个名称不必硬记。关键在“cancellation”，即抵消：证明原本依靠若干项按预期相互抵消，才能继续向下推导。符号的正负有时只是笔误，但如果它决定两项究竟相消还是相加，错误就会击中证明的承重位置。OpenAI称，这处错误还破坏了另外两篇依赖手稿所采用的构造。
因此，仓库撤回了三篇手稿：
- 《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》
这就是数学研究中的“依赖性错误”。一篇手稿常把另一篇的引理、构造或结论当作地基；上游论证一旦失效，下游结果即使没有各自出现新错误，也可能暂时无法成立。
OpenAI没有悄悄覆盖旧文件。仓库记录称，三篇手稿的README已经加入缺陷说明，并链接到存档版本。换句话说，读者仍能看到原稿，也能知道它为什么不再被主张为有效成果。
这不是一次孤立的小修补
同一轮更新中，OpenAI还修订了另外14篇手稿。改动包括修补证明、更正命题、说清假设和依赖关系，以及修正一处已经过时的引文。受这些修改影响，另有13篇手稿更新了对配套论文新版本的引用和版本日期。
这些数字不能简单相加成某个统一的“错误总数”。另一则由Dan Roberts发布的说明将此次更新概括为“19 modifications”，但材料没有解释它与“修订14篇、另更新13篇引用”之间的统计关系。两种说法很可能采用了不同口径，目前无法据此进一步推算。
仓库同时新增6项Lean形式化和5项其他补充内容。OpenAI给出的进度是：719项“顶层结果”中，已有300项完成形式化，约占42%。但“顶层结果”的具体定义没有在材料中说明。这个42%也不等于全部证明已有42%被Lean完整验证，更不能替代数学界的审阅与接受。
Lean能检查证明，为什么仍会撤回？
形式化证明像一套极严格的机器验算。只要某部分被准确写进Lean，证明助手就能逐步检查推导是否符合规则。但它检查的是“已经输入机器的内容”。尚未形式化的手稿、自然语言中的论证，以及形式化命题是否准确对应作者对外声称的问题，都不自动获得保障。
本刊10月8日的报道已经提醒：模型生成手稿、Lean检查通过、数学界接受，是三个不同层次。这次撤回让区别变得具体。仓库仍只有约42%的顶层结果完成形式化，而三篇手稿又因上游关键论证失效被一并撤回。高吞吐发布可以快速展示大量候选结果，却也会把逐项核验的压力一并推向外部。
据Retraction Watch报道，OpenAI曾一次放出722份稿件，涉及372组结果，发布时约一半结果尚未得到形式化确认。数学家Alex Townsend因此认为，公司应优先公布已经通过Lean验证的稿件。如今出现三篇连锁撤回，争议的重点也就不只是“AI会不会犯错”，而是结果应在验证到哪一步时公开，以及发布者应承担多少前置检查责任。
真正要看的，是纠错机制能否跟上发布速度
撤回本身不是科研机制失灵的充分证据。发现核心缺陷、公开说明并保留旧版本，本来就是纠错流程的一部分。OpenAI这次留下缺陷通知和存档链接，也让外界能够追踪版本变化。
但规模改变了问题。当数百份材料集中出现，验证不再只是单篇论文的技术工作，也成为发布机制的设计问题：哪些结果已经形式化，哪些仍靠自然语言证明；哪些手稿依赖同一项上游构造；某个关键错误出现后，能否迅速找出所有受影响结果。这些信息如果不够清楚，核验成本就会落到读者和数学界身上。
所以，这次反转最值得关注的，不是“AI数学行不行”这样过大的判断，而是一条更具体的标准：发布速度可以由模型加快，可信度却仍要靠可追踪的依赖关系、明确的验证状态和公开的纠错记录逐项建立。
局限与未知
- 错误原因及其对另外两篇手稿的影响，目前只有OpenAI自身说明，尚无外部专家或正式勘误文件独立核验。
- 材料没有说明三篇撤回手稿中哪些部分曾完成Lean形式化，也没有交代它们未来是否会修复并重新发布。
- 仓库所称约42%的“顶层结果”已形式化，不代表42%的全部证明已经得到Lean完整验证。