700份手稿48小时，撤回3个结果，验证器赢了

10月8日早上7点左右，一条Hacker News帖子出现了：“OpenAI撤回三项数学结果。”44分，37条评论，到下午就从首页消失了——被模型发布的消息淹没，撤回类消息向来如此。

这三项结果公开了大约48小时。它们属于OpenAI在10月6日发布的内容：一份公告，描述“由内部前沿模型产出的一系列广泛的新数学结果”，以GitHub仓库形式发布——按批评者的统计，一次性超过700个文件——包含手稿、推理轨迹，以及“许多证明的Lean形式化”。

我原本打算写一篇批判稿。公告里有一句话，通常出现在灾难之前：“我们将在获得更多形式化后更新仓库。”读两遍。先发布，验证按滚动时间表进行。这是一家公司发布了700份看似可信的文档，并承诺以后再检查。

但结局与灾难相反。检查器运行了。三项结果死了。而这是这个月AI领域最令人鼓舞的事。

48小时，有记录可查

10月6日10:00，发布。手稿、“许多”证明的Lean形式化——这句话里“许多”这个词承担着实实在在的分量——加上算力估算（他们说每个结果大约需要三小时ChatGPT Pro级别的思考），以及一个咨询小组的咨询。一天之内，GitHub上就出现了镜像和后续追踪仓库。

10月7日，人类数学协会发布声明——托管在Terence Tao的博客上——称这次发布“不是学术的展示，而是权力的展示”，并指出数学家“没有要求做这项工作”。文化战争的框架就此设定：人类对阵不懂数学却做数学的机器。

10月8日早上，三项结果被撤回。追踪仓库的评论者报告，大约42%的顶层结果现在带有完整的Lean形式化。独立审计仓库已经出现——一个发布对某个特定证明的认识论审计，另一个从头重新检查两项结果，在撤回后数小时内更新。

注意这场冲突不是关于什么。没人在争论Lean证明是假的。检查器是机械的：证明要么编译通过，要么不通过，它的git历史精确显示每个形式化何时落地。争论围绕检查器之外的一切——署名、规范、谁要求做这件事。与此同时，检查器本身刚刚公开吃掉了供应商自己的三个头条结果，在48小时的时钟上。

先发布后验证——作为一种特性

这是我觉得真正新的部分，也是为什么这不只是“AI垃圾，但经过同行评审”。

科学已经在验证前发表——这就是预印本。但预印本把状态写在脸上：这还没被检查过。OpenAI发布的东西更接近一份附带仓库的新闻稿，而撤回表明，验证层现在比公关层跑得更快。Lean机械地检查证明。镜像一天内分叉语料库。独立审计者挑选结果并重新推导。社区运行公告推迟的检查，失败以公开提交的形式浮出水面，而不是A18页的更正。

仓库就是收据。它的历史在重要的意义上是只可追加的：三次撤回永远可见，带时间戳，可diff。没人能悄悄把错误证明换成正确证明——审计者持有早期快照。这是一种防篡改属性，偶然达成的，出现在验证完全机械化的那个领域。

这就是全部诀窍，也是这周在数学之外重要的原因：这是第一次大规模演示，“AI提议，系统验证”经受住了一家前沿实验室自尊心的考验。每个人都念这句口号。这周，三个被撤回的结果就是后半句真正运行时的样子。

帖子里没人能回答的问题

撤回帖里有一条评论值得更多关注：“被撤回的那些到底有没有经过Lean检查？这似乎很重要。”

这极其重要，而截至撰写时，它仍未解决。如果这三项结果被形式化了，且Lean批准了它们，那么形式化在语义上出了偏差——证明了一个与手稿声称的略有不同的陈述，即“证明编译通过”与“证明证明了”之间的经典鸿沟。如果它们尚未被形式化，那么撤回更简单：未验证的尾部在检查器到达之前就被撤回了，这没问题，但那样的话，头条数字——“许多证明的形式化”——承载了超出其承受能力的重量。

两个版本教给我同一个我反复艰难学到的教训：没有验证日志的验证声明，只是一个看似可信的叙述。“许多证明被形式化”毫无意义，直到你能问出哪些证明、由什么检查、何时检查——并得到一个本身就是收据的答案。这个问题在数学里有答案。在我们发布的大多数东西里——智能体、审计、合规文档——它仍然没有。

无论你构建什么，可以借鉴什么

把检查器和产物一起发布。仓库的力量来自Lean与手稿并排放置。你的对应物：把复现命令放在基准数字旁边，把验证脚本放在导出文件旁边。

让日志来做撤回。记录在公开历史中的撤回维护信任；静默编辑摧毁信任。diff就是更正。

为未验证的尾部留出预算。“我们将在获得后更新”只有更新计划真实时才是一句诚实的话。OpenAI这周正被按他们的计划问责。在别人替你写下之前，先写下你自己的。

两个诚实的局限

撤回本身是这篇文章里收据最少的事实。我能指向公告、人类数学协会声明、审计仓库——