热点跟踪 015｜被骂了三个月，才有了这次发布：OpenAI 722 份数学手稿的言行审计

先把时间钉住。10 月 6 日，OpenAI 发布博客《Sharing AI progress in mathematics》，同日在 GitHub 公开仓库 openai/math——两天拿下 9832 颗星，这个速度在学术类仓库里非常罕见。对应的 Hacker News 讨论截至 10 月 8 日上午攒了 1241 个支持票、1412 条评论，仍在榜首发酵中。这不是一次例行开源：从 8 月到 10 月初，OpenAI 在数学领域的发布方式被连续批评了三个月，这次大放出发生在批评声浪之后——时间顺序本身就是本期要审的东西。这期也写在一个持续发酵事件的半途，榜单位置还在动，数字以 10 月 8 日上午为切面。以下事实以官方博客与仓库自述为准，HN 反应池数据已独立核对，转引部分正文标注。

发生了什么

OpenAI 把一个内部模型的数学产出整批公开了——722 份研究手稿、归成 372 个结果族，仓库 132,880 个文件、3.1GB，主语言是形式化证明语言 Lean，Apache-2.0 协议。

仓库分三层。第一层是 preprints，722 篇论文的 PDF 加源文件；第二层是 lean 目录，12 万个 Lean 文件按 24 个学科组织，依赖社区数学库 mathlib4 的固定版本；第三层是 reasoning_traces，10 份推理过程的摘要节选——注意官方自己的措辞是「摘要的节选」，不是完整思考过程。验证入口也备好了：官方推荐 comparator 流程，把 comparator、landrun、lean4export 三件工具配进环境，lake update 拉起依赖、lake exe cache get 取社区编译缓存，就能逐条验证结果族。产出这些结果的模型没有发布，官方口径是「未发布的内部前沿模型」；它做了约 4000 道题，平均每个结果花 3 小时 ChatGPT Pro 等效的思考算力。722 篇里 162 篇有 Lean 形式化的主结果，其余 560 篇只有论文本身。博客同时承诺资助系列研讨会，并表示正在推进「负责任地发布产出这些结果的模型」——模型本身何时放出，是埋给后续的钩子。仓库内部结构、验证流程怎么跑，同日的拆解 019 专门写，本篇不展开；本篇的主线是另一件事：这次发布是怎么被骂出来的。

被骂了三个月，才有了这次发布

先把时间线摆出来。

8 月，OpenAI 用 Astra 模型在 Lean 语言里做了十道数学题的演示——形式化工具本身是数学社区的公共基础设施，一家 AI 公司拿它当模型能力的秀场，第一次让部分数学家觉得不对味。9 月 10 日，纳维-斯托克斯方程相关的证明宣称出现——这是流体力学的百年难题，一个未经同行评审的宣称直接面向公众发布，刺眼程度可想而知。9 月 11 日，25 位菲尔兹奖得主发表联合声明，指向 AI 公司在数学领域的发布方式；上次我们写过这件事（热点 003，9 月 12 日）。9 月中旬，数学家对发布方式的批评持续见诸报道，焦点从单次事件转向发布机制本身。然后是 10 月 6 日：博客说这次发布按数学与 AI 顾问组的建议设计。

这条归因链最扎的一点，藏在顾问组建议书本身。据 HN 讨论转引，这个挂靠普林斯顿高等研究院的顾问组（AGMAI）的建议书开头就写了两层意思：明确表示不背书这种做法，并要求停止在专有模型上测试高级数学问题。对照 OpenAI 的实际行为，言行审计的结果很清楚：发布规范那一半——建公开仓库、给引用规范、做 Lean 形式化、附推理摘要、标算力口径——全部采纳了；「别测了」那一半，博客原文专门花段落论证继续在内部前沿模型上测数学题为什么重要。怎么发，听了；别测了，没听。两边各取一半。这个选择本身说明了优先级：程序正义可以谈，测试节奏不让。博客把这次发布描述成与数学界合作的样本，但合作条件里最硬的那一条——停止测试——没有出现在任何段落里。截至发稿，OpenAI 对「停止测试」这个诉求没有任何正面回应。菲尔兹奖得主陶哲轩在 Mastodon 发帖（据 HN 转引），态度比联合声明温和：他希望 AI 能向人类数学家解释结果，也相信 AI 在阐述、社区建设、新研究方向上可以有正贡献——温和归温和，他同样没说「请继续测」。

第三层批评指向「机器可验证」这个卖点。162 除以 722，形式化率约 22%；剩下 560 篇只有 PDF，没有 Lean 证明——换句话说，接近八成的手稿，机器验证这层保险是缺席的。而形式化本身也不是免检章：arxiv 2610.08144 的论文指出，自动形式化的忠实性判定问题在 SCI 层级里是 SCI=∞，比停机问题（SCI=1）还难——用大白话说，判定一份机器翻译有没有忠实还原原论文，比判定程序会不会停下来还要没有通用算法。也就是说，Lean 验证的是形式化之后的陈述，并不能保证这份形式化忠实翻译了原论文。HN 里的同款质疑拿到了高赞：Lean 证书的前提是定理陈述被正确翻译，而跨这么广的领域里没有这个保证。仓库 README 自己也承认：未经形式化的部分可能有错，会尽快修。三方口径在这里罕见地一致——官方、论文、社区都同意验证真空存在，只是官方把它写成了免责段落。

评论区怎么说

HN 一千四百多条评论，几个声音有代表性。

最高赞的一条给 OpenAI 与数学界的互动打了肯定分，但补了一个刀刀见血的条件：这是在被公开骂了之后才做的。另一路意见走得更远：数学界要的从来不是许可，是规范——并指控前任发布流程抢发人类研究者的方向、漏引已有工作（据讨论区转述）。这类积怨不是一次大放出能清零的。

发布渠道本身也有争论：一部分人认为公开仓库加 Lean 代码是数学发布的新范式，另一部分人坚持论文就该上 arXiv 走同行评审，GitHub 替代不了评审，代码的存在感也压不过评审程序缺失的问题。在数学这个以同行评审为信任根基的领域，渠道之争说到底是信任之争。

最有人味的一条来自 PhD 学生：写了一半的论文方向被 722 篇砸中了怎么办。下面的共情很直接——别把研究喂给 AI，它会被拿去训练然后抢发。署名问题也在这里被提起：722 篇论文只署 OpenAI，不署具体研究者；有人建议至少让审校者署名，得到的回应是这等于在训练大众去信任机器而不是审校者；也有人解释，竞争环境下团队名单本来就不便公开。一个署名栏，挤着三套立场。

还有一条流传很广的个人估计：这批结果相当于数学 50 到 100 年的进展——注意，这是单个用户的估计，不是共识，评论区反对声不少。这类量级判断不必急着站队：仓库是公开的，结果会被数学界一篇篇消化，成色如何，时间会给答案。

普通用户能做三件事

第一，亲手验证一条定理。 仓库文档给了完整的 comparator 流程，按 lean/README 的步骤配好环境，一条命令就能验证一个结果族——比如准黎曼假设的 7/8 结果。人类最好纪录是 11/12，7/8 是弱于人类纪录的推进，不是终点。这也是普通读者第一次能对前沿 AI 数学宣称做一手核查——不需要懂证明细节，照文档跑命令就行。README 还专门警告全库编译会撞系统内存映射上限、给了绕开参数——仓库大到要专门写编译避坑文档，这本身就是个注脚。

第二，把 CONTENTS.md 当检索地图。 722 篇不该当杂志从头翻，官方已经按 24 个学科把结果族列好在这份文件里，先按自己的领域找感兴趣的那几条，再进对应手稿。检索优先于通读，是面对这种量级产出的正确打开方式，也是省时间的唯一办法。

第三，对只有 PDF 的结论保持「未经形式化 = 存疑」的阅读姿势。 560 篇没有 Lean 证明的手稿，读法应当是证明宣称，不是已验证事实——这不是刁难，是仓库 README 自己定下的口径。引述、转述、二创传播时把这个标签带上，是普通读者能为信息环境做的最实在的一件事。

结语

分寸最后拿稳。本期记录的是时间顺序和文本对照，不脑补 OpenAI 的动机，也不给它定罪；它对顾问组「停止测试」诉求保持沉默，沉默本身是记录在案的事实，不是我们替它说的回答。被批评之后才有这次发布，这句话是时间线的概括，不是对动机的判决。

两件事接下来值得盯。其一，那个产出 722 篇结果的模型，会不会如博客承诺的那样负责任地发布——发，或者不发，都直接检验「怎么发」的诚意是止步于手稿，还是延伸到模型本身。其二，722 篇里第一篇被证伪或修正的消息什么时候出现——在官方自认未经形式化可能有错的前提下，这个时间点会很大程度决定这次大放出最终被怎么评价：一次诚实的示范，还是一批待检验的宣称。README 承诺的「尽快修」，届时响应得多快，同样在观察清单上。

参考来源

• OpenAI 博客《Sharing AI progress in mathematics》（2026-10-06，Wayback 存档全文，一手）
• github.com/openai/math（一手：README、CONTENTS.md、formalization.yaml、comparator 文档；722 手稿 / 372 族 / 132,880 文件 / 3.1GB / 9832★）
• Hacker News story 49984923（1241▲ / 1412💬，Algolia 数据；评论区观点均为转述去引号，AGMAI 建议书与陶哲轩发帖为讨论区转引）
• arxiv 2610.08144《Navier–Stokes Lost in Translation》（摘要一手；SCI=∞ 结论出处）
• 25 位菲尔兹奖得主联合声明相关报道（9-11；本账号热点 003 已覆盖，回指）
• Astra 十题、纳维-斯托克斯宣称、9 月中旬批评报道（MSN 存档、ForkLog、The Next Web 等二手池，时间线锚点用）