722 篇数学稿：可信度交给证明检查器，而不是发布会

10 月 6 日傍晚（美东），OpenAI 把一批数学稿丢进了 GitHub 仓库 openai/math。The Verge 时间戳是 11:26 PM UTC；仓库创建约在 21:47 UTC。官方页写：未发布的内部前沿模型产出一批新结果；仓库按结果族组织稿件，附修订与引用协议，并放出许多（不是全部）Lean 形式化证明。AGMAI——高等研究院旁那家独立顾问组——称其中包含「数百个」未决问题的解答。

标题党会写成「AI 解决了数学」。OpenAI 自己的句子更克制：sharing AI progress in mathematics。差别不在修辞，在信任放在哪。

TL;DR：放出了什么（稿件、部分 Lean 证明、推理摘要、算力估计），谁验证了什么（形式化部分可机器核，未形式化部分要人读，AGMAI 管沟通不是审稿），意味着什么（发布节奏压过同行评审节奏，署名与先前工作的引用成了伦理问题）。「解决」一类词，本文一律按 OpenAI / AGMAI 自述限定，不替任何结果做数学裁决。

一、仓库里有什么，没有什么

按仓库说明与首发报道：最初目录是 722 篇稿、372 个结果族；族里可以有主结果、伴随论证、推论或另证。后来目录有过撤回与更新，外界转述出现过 719 之类的数字——写的时候以仓库当时 catalogue 为准，把「722」当作首发时的公开说法，而不是永恒定数。

OpenAI 还放了：约 10 份模型推理摘要、按 ChatGPT Pro 用量估的算力、尝试过多少题的统计。官方称平均结果约等于 ChatGPT Pro 三小时思考。这是公司自报的换算，不是独立审计。

没有放进仓库、或至少没有作为审稿结论放进仓库的：同行评审意见、对「是否首次解决」的权威裁决、模型权重本身。官方说正在探索符合顾问组指南的社区托管替代方案；未来披露会改引用、表述与呈现。换句话说，这次选的渠道是 GitHub，不是期刊。

二、信任从机构声誉挪向检查器——只挪了一半

Lean 形式化是这篇材料里真正新的治理动作。一段证明被写成 Lean 4，计算机可以检查推理步骤是否合法。对形式化了的那一部分，信任对象从「OpenAI 说它对」部分转向「检查器说步步合法」。这很重要，尤其在结果批量涌入、没有人能在一周内读完 700 多篇稿的时候。

但官方自己写：many, but not all。未形式化的稿件，仍压在数学家的注意力、声誉和引用网络上。AGMAI 的职责是沟通与发布规范建议——及时披露、尽量走既有学术渠道、公布模型名/提示/算力、不要把数学结果当营销车——不是替每篇稿做数学审稿。

flowchart TD
  M["内部前沿模型<br/>产出结果"] --> F["结果族 / 稿件"]
  F --> L["已 Lean 形式化"]
  F --> U["未形式化"]
  L --> C["证明检查器<br/>机器可核步骤"]
  U --> H["数学家注意力<br/>阅读、挑错、定位先验工作"]
  A["AGMAI<br/>沟通与发布规范"] -.->|不管审稿结论| F
  O["OpenAI 发布会 / 博客"] -.->|不替代核验| F

所以「可信度交给证明检查器」只对了一半。一半交给了机器；另一半仍交给人，而且人面对的是一次性灌进公共域的数量级。验证成本没有消失，它改了分配：形式化部分的边际成本下降，未形式化部分的排队成本上升。

三、单提示、单代理，对照万级蜂群

OpenAI 在相关披露里强调：这批结果几乎都出自单提示、单代理设定——对照此前某些工作里动用大规模代理蜂群的叙事。若属实，它改变的不只是算力故事，还有「谁算作者」的直觉：不是一万个代理开会，而是一条轨迹写完一篇。署名伦理并不因此变简单。模型没有法律人格；提示工程师、对齐团队、写过被引用引理的人类数学家，各自处在不同的贡献层。AGMAI 九月末的建议里，已经点名要求披露模型名、提示与算力，并警告不要把发布当营销。

The Verge 写到，数学界对今年 AI 实验室冲进学科的速度——尤其是发布方式——争论激烈：研究实践、伦理、以及如何给人类先验工作署名。本稿不裁决任何具体定理的优先权；只记录：发布节奏已经跑在传统同行评审前面，引用与修订协议被塞进 README，正是因为旧管道装不下这个流量。

四、证据边界

「解决了数百个未决问题」出自 AGMAI / 报道转述，不是本文的数学判断。
Kakeya、算法改进、RH 方向等具体条目，以仓库 overview 与稿件本身为准；本文不展开、不背书。
算力「三小时 Pro」是 OpenAI 换算；成功抽取率、独立复现率均未作为已核事实写入。
仓库稿件数可能随撤回变动；引用时核对当日 catalogue。

把这些边界写进正文，是因为这类稿最容易在转述里膨胀。实验室有激励把批量结果写成能力展示；媒体有激励写成「突破」；数学家需要的是可检查的对象与可定位的先验工作。三者目标不完全重合。GitHub + Lean 是一次把激励往「可检查」一侧推的尝试，推了多少，要看未形式化队列多长、修订协议是否真被遵守。

五、和治理线的接头

同周还有欧盟文字水印、市议会宣誓听证。看起来一个是合规产品，一个是数学开源，一个是立法取证——共同结构是：证明成本往外推。水印把检测权推给获批机构；数学稿把形式化推给检查器、把阅读推给学界；听证把风险量化推回实验室，实验室又推回「没有严谨方法」。谁付钱、谁排队、谁有权说「够了」，决定了这些推送会不会变成真正的公共品。

本站不把这篇写成「AI 赢了数学」。写成：一次大规模披露，把验证分工摊开给了机器与人；机器接管了已形式化的一半，人仍要吞下另一半，而且发布会替不了任何一侧。