377 个结论、721 篇稿件、其中 300 篇附 Lean 形式化（占当时 719 篇的 41.7%）：一次「AI 数学」发布里，验证究竟验证了什么 - 技术文章

先说人话（打个比方）：假设有人送来一箱论文，说「这些都能证明」。你手里有一个极其严格的检查器，它只认「用严格语言重写过的命题」，而且只检查「这个命题是否被证出来了」。那你现在能保证什么？你能保证重写过的那些命题是真的。你不能保证重写时没有把原命题改弱，也不能保证原来那句话就是你想证明的那件事，更不能保证没被重写的那些。

2026 年 10 月 6 日，OpenAI 一次性公开了一批由内部模型撰写的数学稿件。围观者很快分成两派：一派说「数学被攻克了」，一派说「一堆没人读的论文」。两派都在用一个含糊的词——验证。这篇文章想做的事很窄：把「验证」这个词拆成可计数的几层，然后算清楚每一层的覆盖率，最后给出几条做工程的人可以直接搬走的做法。

如果你的工作里也有「模型产出 + 自动检查 + 人工兜底」这条链路（单元测试、静态检查、LLM 自评、代码评审），那么这次发布其实是一次难得的大规模压力测试——它把一个平时藏在流程里的小问题，放大到了「377 个被宣称解决的开问题」的规模上。

10 月 6 日到 10 月 29 日：时间线与热度依据

先把事实按日期摆开，因为这件事里绝大多数误读都来自「把不同日期的数字并排说」。

日期（2026）	发生了什么	一手出处
10-06	OpenAI 发布《Sharing AI progress in mathematics》，公开一批内部前沿模型产出的数学结果；仓库当天建立	openai.com 官方博客、GitHub `openai/math` 创建时间
10-06	媒体口径：「377 个被宣称解决的开问题」，分布在 722 篇稿件里	Quanta《Deluge of 377 OpenAI proofs bewilders the math world》
10-07	仓库 history 记录：因一处符号错误撤回 3 篇稿件（根因 1 篇 + 依赖其构造的 2 篇，3 篇之内）；同条目另修订 14 篇稿件，随后因这些修补连带更新 13 篇的引用	仓库 `history.md`
10-07	同一份 history：形式化总量记为 `300 / 719 = ~42%`（300 = 带 Lean 形式化的顶层结果所在稿件数；这句的分子分母口径本身混用，见下节）	仓库 `history.md`
10-09	媒体报道「墙上的裂缝」：三篇因「一个放错位置的负号」被撤回，剩余 719 篇	Quanta《Cracks appear in OpenAI’s wall of proofs》
10-12	独立第三方发布抽取式审计预印本，覆盖 38 个族，明确声明「抽取不是验证」	arXiv:2610.17090v1
10-15	OpenAI 追加：向 Simons Foundation 的新计划出资 500 万美元，用于组织数学家理解这批结果	openai.com 官方博客更新段
10-26	新增 2 篇带 Lean 形式化的稿件（含「ETH 为假」一篇，交由 Impagliazzo、Paturi、Williams 三人小组复核）	仓库 `history.md`
10-29	修掉 Comparator 挑战与解答之间命名空间不一致的问题	仓库 `history.md`

热度依据（为什么要写它，而不是别的）：官方博客 10-06 首发、10-15 追加资金说明；第三方媒体在 10-06、10-09、10-19 连续三轮跟进（10-19 那篇把其中一个结果称为「目前为止最重要的 AI 数学成就，领先幅度很大」，引用对象是斯坦福的 Jared Duker Lichtman）；社区侧出现了独立的复现仓库、独立的审计预印本，以及若干公开的 Lean 检查报告。也就是说，这不是一条只发了通稿的新闻，而是已经产生了独立的第三方核查产物——对技术读者来说，这才是值得深读的信号。

四个数字不是一回事：口径先分清

这是本文最想先解决的一件事。同一批材料里至少有四个「数」，分母各不相同：

数字	它数的是	分母/口径	出处与日期
377	被宣称解决的开问题数	按「问题」计（Quanta 口径，不是稿件数，也不是「族」数）	Quanta 10-06，转述 OpenAI 口径
372 → 373	稿件「族」（family）数	族 = 一组相关稿件（可含主结果、伴随论证、推论、替代证明）；注意「族」不是对「问题」分组	第三方审计 10-12 记 372；现仓库 README 记 373
722 → 719 → 721	稿件（manuscript）数	按文件计	10-06 首发 722；撤回 3 篇后 719；10-26 加 2 篇后 721
300	含 Lean 形式化「顶层结果」的稿件数	分子 300、分母 719，即 41.7%	仓库 `history.md`，10-07

四个数放一起，很容易被读成「722 篇里 42% 被验证，所以约 300 篇可信，占 377 个结果的八成」。这句话每一步都错。

第一，377 与 722 不是同一分母：平均一族约 1.9 篇稿件（721/373），一篇稿件不必然对应一个独立结果。第二，41.7% 是「稿件被形式化」的比例，而仓库原文那句把分子分母写成「top-line results / 719」——719 是稿件数，不是结果数，这句话自身就把两个分母混在一处了。第三，「被形式化」不等于「被独立复核」：形式化是发布方自己放进去的产物。

所以本文后面一律这样表述：「300 篇稿件（占当时 719 篇的 41.7%）带有 Lean 形式化」，不再简写成「42% 被验证」。这不是抠字眼，因为下一节会看到：这三个词（形式化、机器检查、独立验证）在这件事里的差距，恰好是整个故事的技术核心。

术语与符号约定

后面会反复用到几个量，先约定。每个术语第一次出现时还会再给一句定义，这张表只是方便回查。

记号 / 术语	含义	备注
$K$	被宣称的结果数	本例取 377
$N$	实际被尝试的问题数	本例约 4000
$M$	稿件数	时间相关：722 / 719 / 721
$c$	形式化覆盖率	$\approx 300/719 = 41.7\%$
$f$	陈述忠实度	形式命题与原英文命题语义一致的概率，取值 $[0,1]$
$A$	有效保证	本文定义为 $A=c\cdot f$ ，见第五节后
形式化	formalization	把非形式命题翻译成证明助手的语言（此处为 Lean 4），并写出机器可查的证明
内核	kernel	证明助手里唯一被信任的那一小段代码，只负责逐条检查证明步骤是否合法
公理许可表	`permitted_axioms`	检查器允许解答使用的公理白名单，超出即判不通过
可信基	TCB	trusted computing base：必须为真、否则整套检查失去意义的那些前提
族	family	一组相关稿件的集合，可含主结果与推论

验证的四层阶梯：从「声称」到「进入文化」

从事数学的人其实早就有一套分层语言。伯克利（UC Berkeley）的 Olga Holtz 在 Science 2026-10-13 的报道里给出的那句区分很值得直接搬过来（媒体转述，非笔者原意提炼；该报道本轮直接请求返回 403，此句经检索摘要与多家转载一致核对）：

「必须区分『被声称的结果』『被独立验证的结果』和『被理解并吸收进数学文化的结果』。这三者不是一回事。」

这句话可以直接形式化成一个四层阶梯，每一层的判据不同、成本差一到两个数量级：

验证的四层阶梯：L0 被声称、L1 被机器检查、L2 被独立复核、L3 被吸收；每层的判据分别是作者、Lean 内核、外部读者与数学社区，代价依次为写下、翻译成形式语言、有人愿意读、以年计的时间 — 图 1　验证的四层阶梯：每上一层，判据换一个角色（本文自绘）

需要先说明一个本文的处理口径：仓库只提供了「稿件附带 Lean 形式化」这个事实，没有提供逐篇「跑过 Comparator 并通过」的执行记录。因此下文把那 300 篇一律按 L1 的「产物」 记，而不是按 L1 的「执行结论」记——差一层证据，就不能多算一层保证。

这张图想说明的一件事：每一层都是一次「判据换人」。L0→L1 换成了内核，代价是把命题翻译成形式语言；L1→L2 换成了外部读者，代价是他们必须愿意读；L2→L3 换成整个社区，代价是时间。任何一层没跨过去，前面那层的结论都还在原地——不会自动往上传导。

把这件事写成一个单调的覆盖率链条：

A_{\text{effective}} = c \times f \times r \times u

其中 $c$ 是「有多少稿件带形式化」、 $f$ 是「形式命题与原文是否同义」、 $r$ 是「有多少被独立重跑」、 $u$ 是「有多少被真正读进去」。四个因子全部小于等于 1，所以任何一层没做，最终保证就被乘掉。

这个式子最大的用处不是算出一个数（这几个因子都测不准），而是逼你把「验证到什么程度」说成一个向量而不是一个布尔值。只说「已验证」，等于把四维信息压成一维，而且压掉的正是不确定的那三维。

一条形式化检查流水线在检查什么

要谈「机器检查」，得先看清那个检查器到底在检查什么。这批稿件的形式化用的是 Lean 4，配套的独立检查器叫 Comparator（该项目 README 明确写了它已在 Lean v4.35.0 起并入核心，成为 lake comparator 与 lake check）。

它的工作方式非常「工程」：把证明拆成挑战（challenge）与解答（solution）两个模块。

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": ["todo1"],
  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
}

Challenge.lean 里写下你要证明的命题（可以是 sorry，即暂不证明）；Solution.lean 由声称证明了它的人提供，写下同一个命题加上完整证明。检查器比对三者：命题是否同一、公理是否超出白名单、内核是否接受。

关键在于它的 README 把「成立条件」一条条列了出来——这正是本文最想强调的部分。检查成立需要六个前提同时为真：

Challenge.lean 的传递导入闭包与 lakefile 由你（信任方）控制；
你没有先编译过任何可能带对抗性的文件（否则挑战文件可能被污染，让你以为在查 A 命题、其实在查 B）；
landrun 与 lean4export 在 PATH 里；
landrun 本身工作正常，且解答没有利用它的沙箱逃逸漏洞（README 注明它用 systemd-run 额外挡了一个「将在 Linux 7.1 修掉」的漏洞）；
Lean 内核正确（若同时挂外部内核，可放宽成「内核与外部内核至少一个正确」）；
不以特权用户运行。

Comparator 的六个前提 A1–A6 同时为真时，才输出命题同一、公理不超白名单、内核接受三条结论；任一前提不成立则结论作废 — 图 2　「机器检查通过」的六个前提：缺一条，结论就不成立（本文自绘）

这张图想说明的一件事：「机器检查通过」是一个有前置条件的结论，不是一个绝对事实。检查器本身写得再严谨，也只有当这六条前提都成立时，它的「通过」才有意义。软件工程里这叫可信基（TCB）——你不可能验证一切，只能把信任收敛到一小块，然后审计那一小块。这里那一小块不是代码，而是六句自然语言的假设。

顺带一个只有真跑过的人才会写进 README 的细节：Lean 仓库 README 专门留了一段技术说明，说整库编译在 Linux 上可能因 vm.max_map_count 太小而失败，解法是用 -DMMAP=OFF 重编 Lean，或设 GLIBC_TUNABLES=glibc.malloc.mmap_max=0:glibc.malloc.arena_max=1。这类「验证工具链自己也会被系统参数绊倒」的细节，比任何宣传语都更能说明形式化验证目前的工程成熟度。

推导一：有效保证为什么必须写成乘积

上一节把检查器拆成了「六条前提」，这一节把「覆盖率」和「忠实度」合成一个可算的量。

设：

$c$ ：稿件中带形式化的比例，已知 $\approx 0.417$ ；
$f$ ：给定一篇带形式化的稿件，其形式命题与原文命题同义的概率；
注意 $c=300/719$ 是稿件级覆盖率（分子分母都是稿件数），所以下面算的是「随机抽到的一篇稿件」而不是「一个结果」。

那么「随机抽到的一篇稿件获得了实质保证」的概率不超过：

P(\text{实质保证}) \le c \cdot f

代入 $c=0.417$ ：若 $f=1$ （完全忠实），上限是 41.7%；若 $f=0.9$ ，上限降到 37.5%；若 $f=0.7$ ，只剩 29.2%。也就是说，忠实度每掉 10 个百分点，整体保证就掉 4 个百分点以上——因为它是乘法，不是加法。

这个式子的第二个用处是给「补形式化」定优先级。Quanta 在 10-06 的报道里转述 OpenAI 的说法：预计形式化其余结果「没有重大障碍」（这是媒体转述，仓库 history.md 里没有这句话；剩余未形式化 419 篇是本文按 719−300 算出的）。但若 $f$ 明显小于 1，那么把 $c$ 从 0.417 推到 0.8 的收益，会被 $f$ 直接打折。先修忠实度、再补覆盖率，比反过来划算——这一点在软件里同样成立：先把「测试断言的语义对不对」搞清楚，再去加测试数量。

失败模式 A：一个符号错如何放大成三篇撤稿

10-07 的撤回记录值得逐字读一遍。原文说：在《Algebraicity of Weil classes on split abelian eightfolds》里，一处符号错误使一个「稳定化迹抵消」论证失效，而这个论证又是另外两篇稿件所依赖的构造。于是共撤回三篇：

《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》（依赖）

这不是「三篇都写错了」，而是「一篇错了，两篇的地基塌了」。把它写成一个依赖闭包：

B = 1 + \sum_{j \in \text{dependents}} \mathbb{1}\left[\text{dep}(j) \cap \text{invalid} \neq \varnothing\right]

本例中 $B=3$ ，即根因 1 篇、有效扇出 2 篇。若这批稿件的平均扇出为 $\kappa$ 、依赖链深 $L$ ，且假设每层独立引用，则期望爆炸半径为：

\mathbb{E}[B] \approx 1 + \kappa + \kappa^2 + \cdots + \kappa^{L}

当 $\kappa=2$ 时，两层就已经是 7。这意味着依赖图的形状，比单篇论文的正确率更能决定一次批量发布的返工量。本例的闭包是 3 篇（1 篇根因 + 2 篇依赖），占首发 722 篇的 0.41%（注意这个 0.41% 与 300/719 = 41.7% 无关，两者只是分母数字相近，极易看混）。

这里要特别小心一处容易读错的因果：同一份 history.md 的 10-07 条目里还有另外两组数字——另修订 14 篇稿件（证明修补、陈述更正、假设与依赖澄清），以及「因这些修补而连带更新 13 篇的引用」。这两组属于同一次维护动作，但不是那 3 篇撤稿的下游。把它们并成一条因果链，会把一次 3 篇的依赖事故夸大成 17 篇的连锁反应。

左侧：一处符号错误经依赖闭包放大成 3 篇撤稿；右侧：同一 history 条目下另修订 14 篇、连带更新 13 篇引用，与撤稿无因果关系 — 图 3　撤稿的爆炸半径是依赖闭包，14 篇修订不是它的下游（本文自绘）

这张图想说明的一件事：撤稿的爆炸半径是依赖闭包（本例 3 篇），而 14 篇修订与 13 篇引用更新是另一组维护动作——两者同时发生，但不是同一条因果链。

这条对做工程的读者几乎是原样可搬的结论：批量产出 + 交叉引用 = 错误不再是局部缺陷，而是可达性问题。你有一份「模型生成的 700 个模块，互相 import」，其中一处的接口签名错了，坏掉的可能是一整条依赖链，而 CI 只会告诉你「这 700 个模块都编译通过」。

失败模式 B：陈述忠实度不可自动化

这是本文认为最被低估的一层。

Lean 内核检查的是代码里那个命题。它不知道这个命题是不是论文第 3 页里那句定理。要把两者对应起来，必须先做一次「非形式 → 形式」的翻译。这一步：

不可自动化。Mathlib Initiative 主任 Johan Commelin 在媒体采访里的说法是：「这不是能自动确立的事，需要人读 Lean 代码。」（其身份据 Quanta 10-09 报道的称谓；他长期主持形式化项目，不是分布式系统方向。）
可能被悄悄做弱。第三方与媒体都提到，被测的形式化里存在「形式化出来的是比主定理更弱的东西」的情况——形式上没错，但力度不够。
可能对不上原文。有报道称，Navier–Stokes 相关结果的 Lean 形式化与配套论文里描述的证明并不一致；这不代表结果错，但它说明**「有 Lean 证明」不能直接当「论文那句话被证了」**。

把它写成一个两段式条件。设 $T$ 为「英文命题为真」， $T'$ 为「形式命题为真」， $E$ 为「内核接受该形式证明」。用链式法则，两者同时成立的条件概率是：

P(T \cap T' \mid E) = \underbrace{P(T' \mid E)}_{\text{内核能给的}} \times \underbrace{P(T \mid T', E)}_{\text{只能人给的}}

第一项可以很接近 1（内核接受是很强的证据），第二项没有任何机器保证。所以「有 Lean 证明」这句话的强度，最多等于第二项。这在工程上有一个几乎一一对应的类比：测试通过证明的是「代码满足你写下的断言」，而不是「代码满足你想要的规格」。断言写错了，测试越绿越危险。

举一个最小的例子说明「改弱」长什么样。设原命题是「对所有 $n \ge 2$ ，该不等式成立」；形式化时若写成「对所有 $n \ge 10$ ，该不等式成立」，内核完全接受这个证明，检查器也报通过——但被证明的东西比原命题弱了一大截，而这个差异在代码里看不出来，只有把两句并排读的人才看得见。另一种不等价不是「更弱」而是方向不明：把「对所有素数」写成「对所有大于 2 的素数」，在整数范围内其实等价；把「对所有 $n \ge 2$ 」写成「对所有 $n \ge 10$ 」则是削弱。两种情况的代码都「通过检查」，而只有把两句并排读的人才分得清哪一种是原意。

这类「弱化」不是造假，也不需要动机——它是翻译过程里最自然的一种损耗。所以任何形式化项目都必须配一步陈述比对（把英文命题与 Lean 命题逐条对读），而这一步恰恰是唯一无法交给机器的部分。

失败模式 C：定义洞与「规范游戏」

Comparator 的 README 还写了一段很少被引用、但对做产品的人极其有用的警告：它支持「定义洞」（definition hole）——挑战方把某个定义留空，让解答方填。检查器可以保证填的东西公理不超集、内核接受、名称与类型匹配。但 README 明确写着：

很多定义洞的挑战，在缺少额外监督的情况下是可以被「做局」的。

它的例子很具体：挑战方留下 def ChallengeSolution : Prop := sorry，并断言 theorem challenge : RiemannHypothesis ↔ ChallengeSolution := sorry——本意是让解答方回答 True 还是 False。而解答方可以直接把 ChallengeSolution 定义成 RiemannHypothesis（黎曼猜想本身），再用反身性一行证完。这一步在形式上完全合规：命题等价成立、公理没超、内核接受，但它没有回答挑战想问的那个问题。README 因此定了一条硬规定：所有定义洞的解答，必须再由一个额外的（可能是人工的）验证者检查。

这类问题在任何「按规格验收」的系统里都存在，而且是最难用自动化堵住的一类：规格本身可以是攻击面。把它和上一节合起来看，会发现一个共同结构——形式化把「对不对」变成了「在这个规格下对不对」，于是规格的忠实性就成了新的单点。这和「测试覆盖率 100% 但断言全是 assert True」是同一个失效模式。

推导二：从 4000 次尝试到 377 个结论，筛选是承重墙

现在看另一条线：这批结果是怎么从「尝试」里被选出来的。

公开信息是：整个评测过程里模型被喂了约 4000 个问题；把输出聚合成「族」与「稿件」，并要求「appropriate level of significance」，最后得到 377 个结果。媒体转述里还有一句很关键的补充：模型在尝试的绝大多数问题上都失败了。

于是「公开结果数 / 尝试问题数」是：

\frac{K}{N} = \frac{377}{4000} \approx 9.43\%

这个比值只能说明公开集相对尝试集很小；它不等于「每次尝试的成功概率」，因为一个问题被尝试几次、几个问题被并进一个结果，本文所查的材料都没说清。真正有据的定性结论来自媒体那句「绝大多数失败」，而不是这个比值的小数点。

不过这个比值指向的那件事是真的：整个可信度压在一个几乎不可审计的环节上——筛选。把筛选写成一个最简模型：设 $\tau$ 为问题集合里「确实可解」的先验占比， $\epsilon$ 为「不可解的问题被错误地宣称解决」的概率， $1-\delta$ 为「可解的问题被正确宣称解决」的概率。若公开集就是「所有被宣称解决」的项，则其假发现率为：

\mathrm{FDR} = \frac{(1-\tau)\,\epsilon}{\tau\,(1-\delta) + (1-\tau)\,\epsilon}

代入一组示意值（ $\tau=0.1,\ \delta=0.05$ ）： $\epsilon=0.05$ 时 $\mathrm{FDR}\approx 0.32$ ； $\epsilon=0.01$ 时 $\mathrm{FDR}\approx 0.08$ 。注意这里 $\epsilon$ 缩小 5 倍（0.05→0.01），FDR 只缩小约 3.9 倍——不是同比例，因为分母也在变。所以准确的说法是：在 $\tau$ 固定、 $\epsilon$ 较小时，公开集的错误占比近似随 $\epsilon$ 同向下降。

「appropriate level of significance」这句本身没说是什么检验。下面是本文的假设性示例，不是对 OpenAI 做法的描述：若把筛选建模成 $m$ 个独立检验、并用最保守的 Bonferroni 校正，单次阈值需收紧到

\alpha' = \frac{\alpha}{m}

取 $\alpha=0.05$ 、 $m=372$ （按族数），得 $\alpha' \approx 1.34\times10^{-4}$ 。再验证这个阈值的效果：即使每次检验的假阳性率被压到 $\alpha'$ ，372 次里至少出现一次假阳性的概率是

1-(1-\alpha')^{372} \approx 4.88\%

刚好回到「5% 以内」——这说明「按族数做 Bonferroni」这种口径在数学上自洽。但它不能用来评价实际筛选有多严： $m$ 到底取 372 还是 4000、用的是 Bonferroni（对单次阈值做除法校正）还是 BH（Benjamini–Hochberg，控制错误发现率而非单次错误率）、阈值定在哪个数，本文所查的 README、history.md、官方博客与审计预印本中都没有说，故此处只作示例、不作判断。

推导三：算力账——「每个结果 3 小时」到底意味着什么

官方口径是：平均每个结果使用了约等于 3 小时 ChatGPT Pro 思考的算力。这句话常被读成「很便宜」，值得算一遍。

若 377 个结果各 3 小时，与这些已公开结果直接关联的算力合计是：

C_{\text{reported}} \approx 377 \times 3\ \text{h} = 1131\ \text{Pro-hour}

但模型实际被问了约 4000 个问题。把上面这笔结果侧的算力摊到 4000 个问题上，得到的是一个比值：

\bar{c} = \frac{1131}{4000} \approx 0.283\ \text{h} \approx 17\ \text{min}

这里必须说清两件事，否则就会算错：先说前提——这段推导假设官方那句「平均每个结果约 3 小时」是把全部尝试（含失败）的算力摊到 377 个结果上的均值；若官方只计结果本身的生成算力、失败尝试另计，则总账高于 1131 Pro-hour，单次成本也高于 17 分钟。公开材料无法区分这两种口径。第一，这个 17 分钟不是「单次尝试的平均成本」——失败的尝试同样消耗算力，而公开材料只说了「每个结果 3 小时」，没说总消耗，所以真实单次成本只会更高，不会更低。第二，它唯一可靠的用途是提醒分母：同一个「3 小时」在「按结果」与「按尝试」两个分母下相差 10.6 倍，引用时必须说清是哪一个，否则读者对成本的直觉会错一个数量级。小结与「误读三」里对这两个数的复述，都以上述假设为前提。

这笔账还有第二半，而且更要紧：验收成本没有被计入。设生成成本 $C_g$ 、形式化成本 $C_f$ 、人工复核成本 $C_h$ ，总成本应是

C_{\text{total}} = C_g + c\,C_f + c\,f\,C_h

其中 $c\,C_f$ 是那 41.7% 的形式化开销， $c\,f\,C_h$ 是「形式化且忠实」的那部分所仍需的阅读开销。已知生成侧是 1131 Pro-hour 量级；而形式化 300 篇、并要求专家读 Lean 代码——这一项的耗时在本文所查的四类材料里找不到任何量化。这也是本文最想提醒的一点：当生成成本下降而验收成本刚性时，瓶颈会从「能不能做出来」搬到「有没有人验收」。

推导四：版本链本身是一份资产

这批材料里有一个很容易被忽略的设计：修订以版本的形式记录，旧版本保持可访问。README 说「我们会保留这批材料的公开发布历史」，history.md 则逐条记着哪天撤了哪三篇、改了哪 14 篇、连带了哪 13 篇的引用。仓库路径下每一篇稿件都有自己的 README，说明缺口并链接到被撤回的旧稿。

把它形式化一下。设第 $i$ 次发布的内容为 $m_i$ ，版本链为：

h_i = H\left(h_{i-1} \,\|\, m_i\right), \qquad h_0 = \varnothing

只要 $H$ 是抗碰撞的，这条链就给出一个性质：任何人想悄悄改掉第 3 版的内容，都必须让后面所有版本的哈希全部对不上。这是把「我们改过，但改了什么你不知道」这种状态，变成「你可以自己算一遍」的状态。

这在工程上的对应物是 append-only 的审计日志（不可改写、只追加），而不是「UPDATE 一行改掉旧值」。差别不在于是否有改动——任何系统都会改动——而在于改动是否留下可验证的痕迹。这批材料在这件事上做得比大多数软件发布流程更严：它没有删掉撤稿，而是让撤稿本身成为公开记录的一部分。

反过来看，这份链也解释了为什么「撤回三篇」这个动作值得单独表扬：一个愿意公开撤稿的产出方，比一个只公开成功案例的产出方，提供的信息更多。因为撤稿记录告诉你两件用别的方法拿不到的事：第一，已公开的撤回占比有了实测值（3 / 722 ≈ 0.41%；这只是「已被发现并公开撤回」的部分，未发现的错误不受它约束，因此它是下界性质的观察值，不是错误率上界）；第二，错误类型是什么（本例是符号错误导致一个抵消论证失效，属于可定位、可修补的类型，而不是「结论方向反了」这种更麻烦的类型）。

把四层阶梯做成一张验收表

前面几节把「验证」拆开了，这里合成一张表，方便直接在项目里对照。表的每一行是一层，列是「谁能做、能自动化到什么程度、失败时症状是什么」。

层级	判据来源	可自动化程度	典型成本	失败时的症状
L0 被声称	有人写下命题	全自动（生成即得）	生成成本	稿件数量暴涨，无人阅读
L1 被机器检查	内核 + 公理白名单	高（但命题需人工翻译）	形式化 + 编译	「有证明」但命题被改弱
L2 被独立复核	外部的人重跑检查	低（依赖外部意愿）	专家时间	通过率无法对外证明
L3 被吸收	同行引用并使用	不可自动化	数年	结论悬空，无法判断价值

这张表的用法不是打分，而是定位你的项目卡在哪一层。大多数团队卡在 L1→L2：检查能跑、机器是绿的，但没有人独立重跑过，于是「通过」只在自己家里成立。而这批材料恰好把 L2 的成本暴露得最清楚——从 10-06 首发到 10-12 预印本的 6 天里，那份抽取式审阅覆盖了 10.2% 的族（是「审阅」不是「复核」，见下一节），剩下的约 89.8% 只能等。

这里不做人力外推，因为做不了：那份第三方审计用的是「每族一次独立的 AI 阅读 + 文献检索」，不是人类逐页精读，也没有公布工时（其 §4 明确写了初始抽取由 AI 逐族完成）。把它折成「等效全职复核者」需要三个本文没有的数：人时、全职率、以及人工复核与 AI 抽取的速度比。少任何一个，算出来的都是假数字——所以这一栏留空，只保留可以核实的那一半：38/372 ≈ 10.2% 的族覆盖率。

这恰好是这一节想说的：一张验收表里最该空着的地方，往往被填得最随便。

第三方审计的覆盖有多厚

10-12 出现的独立预印本（arXiv:2610.17090v1）是这批材料里最值得看的一份「第三方视角」。它做的事情是抽取式审阅：从 372 个族里选了 38 个族，逐族写卡片，记录「哪些是新的证明工具、哪些是已有工具的组合」，并建了一个「验证与依赖计分板」，同时明确写下三条自我限制：

这些稿件没有经过同行评审；
抽取阶段没有编译任何 Lean 工程；
覆盖范围是 38 / 372 ≈ 10.2%，且偏向知名问题。

这份审计的诚实程度值得单独表扬——它没有把「我抽了 10%」包装成「我核过了」。但也正因为诚实，它不能承担两项常被误加给它的功能：

第一，它不是第二层（L2）的独立复核。它明确写了抽取阶段「没有编译任何 Lean 工程、也没有做内核检查」，而 L2 的定义是「外部的人重跑检查」。它做的是「读懂论证并归纳证明工具」，价值很高，但类别不同。

第二，它不能用来估计总体缺陷率。它只覆盖 10.2% 的族、且明说偏向知名问题（不是随机抽样），初始抽取又由 AI 完成。用「38 个样本 0 缺陷」去套三法则（ $3/38 \approx 7.9\%$ ）在算术上没错，但前提——随机、独立、同分布、且真的逐条检测了缺陷——一条都不成立，所以这个数只能当统计课的示例，不能当这批稿件的缺陷率上界。本文把它从结论里撤掉，只在方法层面保留这条提醒：抽样比例不等于证据强度，样本的选取方式才是。

一份可以直接抄的「验证记录」格式

前面几节其实给出了一个结论：「验证过了」这句话，只有在连带说清「验的是哪一层、由谁做、覆盖多少」时才有信息量。所以最实用的落地物不是流程改造，而是一份记录格式——每次自动检查通过时把它填上、随产物一起存。

{
  "artifact": "2026-11-02-openai-math-release-what-verification-verified.md",
  "claims": 377,
  "checked": {
    "layer": "L1",
    "spec_sha256": "...",
    "spec_reviewed_by": "human:someone",
    "coverage": 0.417,
    "statement_faithfulness": "unverified",
    "axioms_allowed": ["propext", "Quot.sound", "Classical.choice"],
    "toolchain": "comparator 4.35.0 / kernel lean4",
    "sandbox": "landrun + systemd-run"
  },
  "independent_rerun": { "by": null, "date": null },
  "human_read": { "by": null, "date": null },
  "known_gaps": ["419 篇未形式化", "4 处族/结果计数未对齐官方说明"]
}

这份格式里有三处是刻意的：

第一，spec_reviewed_by 与 independent_rerun 是两个不同字段。前者问「命题写对了吗」，后者问「别人重跑过吗」。合并成一个布尔字段，就等于放弃了区分这两类风险的能力——而这批材料里出问题的地方，恰好都落在前者。

第二，statement_faithfulness 允许填 unverified。这是整份格式里最重要的一条：让「不知道」成为一个合法的、必须显式写出来的值。默认值必须是 unverified 而不是 verified——因为漏填时的默认值，才是一个系统的真实安全姿态。

第三，known_gaps 是必填。这批材料的仓库在这件事上做得很好：它自己写着「并非所有稿件都有 Lean 形式化」「部分未形式化的结果可能有问题」。把缺口写进产物清单，比在宣传语里回避它，长期成本更低——因为缺口迟早会被别人发现，而那时你有没有提前说过，决定了这次是「已知风险」还是「虚假陈述」。

对做工程的我们意味着什么：五条可迁移的做法

这一节是全文的落点。上面拆出来的东西，其实是一套通用的「模型产出 → 自动检查 → 人工兜底」设计问题：

一、把「验证」输出成向量，而不是布尔值。 每次自动检查通过时，同时记录四个量：覆盖了哪些输入（ $c$ ）、检查的是不是你真正想验的规格（ $f$ ）、谁独立重跑过（ $r$ ）、谁读过结果（ $u$ ）。只写「CI 绿了」，等于把三层不确定性折叠掉。

二、断言与实现分离，且断言要单独评审。 形式化里的「挑战模块」就是这个模式的极致版本：先把命题钉死在受信任的一侧，再让不可信的一侧提供证明。工程对应物是「测试文件由另一个人写」，或者至少「规格变更走单独的评审」。

三、依赖闭包要当指标，而不是当背景。 这批材料里，一个符号错让 3 篇稿件一起下线（1 根因 + 2 依赖），而同一份维护记录里另有 14 篇修订、13 篇引用更新——两组数字常被并成一条因果链，其实来源不同。你的代码库里同一个事实是：一个错误契约的扇出。把「这次改动影响多少个下游」做成可以在 CI 里读的数字，比单看「测试通过率」有用得多。

四、成本模型必须含验收。 生成侧的账好算（1131 Pro-hour 这种），验收侧的账几乎没人算。若你的链路是「模型批量产出 PR / 文档 / 配置」，请把「人读一遍要多久」写进成本模型——否则优化方向一定是错的（你会一直优化生成，而瓶颈在验收）。

五、明确写出信任边界，并逐条审计。 Comparator README 老老实实列了六条前提，包括「沙箱可能有漏洞」这种对自己不利的话。这是很好的工程范式：与其宣称「我们的检查不可能出错」，不如列出「我们的检查在这些前提下成立」，让下一个人知道该从哪里开始怀疑。

三种常见误读，逐一拆掉

在这批材料的传播里，有三种读法反复出现。把它们拆掉，比再加一层结论有用。

误读一：「377 个结果都被证明了」。 这是把 L0 当成 L3。公开材料支持的最强表述是：377 个结果被声称解决，其中一部分有 Lean 形式化，形式化里有一部分被第三方看过。任何把这句压缩成「已证明」的表述，都跳过了至少两层。

误读二：「42% 被机器验证，所以剩下 58% 不可信」。 这是把「未形式化」读成「错」。反过来才对：未形式化只意味着没有机器证据，它的真伪仍由人来判。Quanta 转述 OpenAI 的说法是「预计形式化其余结果没有重大障碍」——那是预期，不是结论。正确的表述是「未形式化部分的真伪目前没有自动化证据」，而不是「不可信」——这两句在对外沟通里的后果完全不同，前者是进度问题，后者是指控。

误读三：「三小时就出一个结果，所以很便宜」。 这是分母错误加上验收成本缺失。三小时是每个被公开结果的平均值（官方措辞只说「平均每个结果」，未说明是否含失败尝试的算力），把它摊到 4000 个问题上得约 17 分钟——这个摊法本身还依赖一个未言明的假设；而形式化与人工阅读的成本，在本文所查的 README、history.md、官方博客与审计预印本里都找不到任何量化。把这两条补上，「便宜」这个判断基本就站不住了。

这三种误读有一个共同点：都是把多维信息压成一维——压成「证明了 / 没证明」，压成「可信 / 不可信」，压成「贵 / 便宜」。本文前面所有公式的作用，就是不给这种压缩留空间。

边界与未解

写清本文的边界，因为这篇稿子的价值取决于读者知道它没做什么：

没有做端到端实测。 文中所有性能与规模数字（377、722、719、721、300、41.7%、约 4000、3 小时、10.2%、7.9%）都是转述或由转述数字导出的算术，标注为「本文自行推导」的部分只有：9.43% 这个比值、17 分钟这个折算值、 $\alpha'$ 与 4.88%、3/38 的上界，以及所有公式本身。
没有编译任何 Lean 工程，因此不对「这 300 篇的形式化是否真能通过检查」下任何判断。
没有逐篇阅读稿件，因此不对任何具体定理的真伪表态。媒体提到的「Navier–Stokes 形式化与论文不一致」一条，本文按「第三方报道」转述，未独立核实。
未核实：显著性判据的具体形式（ $m$ 取值、校正方法）与形式化 300 篇的判定细则（是否含辅助引理、是否要求零 sorry）。这两项在本文所查的 README、history.md、官方博客与审计预印本中均未找到；这是检索边界，不等于官方确定未公布。
未核实：377 与 373 的关系。 现仓库按「族」计 373，媒体按「结果」计 377；两者差 4，本文没有找到官方对这两个计数的正式说明，故全文分别标注口径、不互相换算。
未核实：Comparator 的六条前提在批量核查中是否逐条执行，尤其是 A2（「未先编译过任何可能带对抗性的文件」）——这条在单人手工核查时容易满足，在批量流水线里恰恰最难保证，而本文所查的材料里没有给出该项的执行记录。
一处口径合并需要说明：本文多处把「形式化」与「机器检查通过」当同一件事叙述，但严格说前者是产物（仓库里有 Lean 文件），后者是一次执行的结论（跑过 Comparator 且通过）。公开材料提供了前者，未提供逐篇的后者。
时间锚点说明：本文所有日期均为 2026 年，以官方仓库 history.md 与官方博客为准；引用媒体口径时会写明其发布日。

还有一个更根本的未解问题，值得留给读者自己想：当产出速度比验收速度快一个数量级时，「公开」这个动作本身的含义是什么？ 10-09 那篇报道里引了一位代数拓扑学家的话，大意是「我们没有资源去纠正记录」——这句话说的是审稿能力，不是数学能力。这批材料真正的压力测试对象，可能不是模型，而是学术共同体与工程团队的验收带宽。

小结

如果你只记三件事：

四个数四个分母：377（结果）/ 372–373（族）/ 722–719–721（稿件）/ 300（形式化稿件，占 719 的 41.7%）。混用必错。
机器检查是有前提的结论：Comparator 明确列了六条信任前提；它检查的是「代码里那个命题」，陈述忠实度只能由人给，所以有效保证是乘积 $c\cdot f$ ，不是布尔值。
筛选与验收才是成本中心：4000 次尝试筛出 377 个结论（9.43%），「每结果 3 小时」摊到每次尝试只有约 17 分钟；而形式化与人工阅读的成本，在本文所查的材料里找不到任何量化——这才是这类链路目前真正的瓶颈。

回到开头那个比喻：检查器能保证「重写过的命题是真的」，但它保证不了「重写时没把话改弱」，更保证不了「没重写的那些」。把这句话写进你自己的流水线文档里，比多买一层自动化有用。

最后补一句方法上的自我提醒。本文花了很多篇幅在分母上，看起来像在纠缠细节；但这次发布里真正被传播错的，恰恰都是分母：377 与 722 被当成同一批东西、41.7% 被说成「结果被验证」的比例、「3 小时」被读成每个问题的成本。当一个结论的传播速度远快于它的核验速度时，最先失真的从来不是结论，而是量纲。 这也解释了为什么这批材料里最值得抄的不是任何一个数学结果，而是那份把「已声明 / 已形式化 / 已复核 / 已吸收」分开记账的做法。

📋 来源与核验记录

本节是核验记录（附录性质），不属于教学章节。以下来源均为本轮实际打开核对（2026-11-02，北京时间），按性质分四类。

一、发布方一手材料

OpenAI 官方博客《Sharing AI progress in mathematics》（页面署 2026-10-06，含 2026-10-15 更新段：向 Simons Foundation 新计划出资 500 万美元）。以下取自此文：由内部前沿模型产出、咨询了 IAS 的 Advisory Group on Mathematics and AI、以 GitHub 仓库形式发布并附修订与引用协议、用 Lean 形式化其中许多证明、发布 10 份推理摘要、平均每个结果约等于 3 小时 ChatGPT Pro 思考算力。⚠️ 取数说明：该站对无浏览器 UA 的自动化请求返回 403，本轮用 curl 取到 200 与全文（332 KB 原始 HTML），因此 verify-article-sources.py 会把它报成「HTTP 403 异常 1 条」——这是站点反爬策略，不是链接失效。https://openai.com/index/sharing-ai-progress-in-mathematics/
GitHub openai/math 仓库 README（本轮读取版本：721 篇稿件 / 373 族；「~42% top-line results formalized」；约 4000 个问题；平均每结果约 3 小时 Pro 算力；两处例外为黎曼 ζ 函数的无零点区域与 CM 阿贝尔簇上的 Hodge 猜想；其中一篇写作为可读性经人工编辑）。https://github.com/openai/math
同仓 history.md（本轮读取）。以下取自此文：10-07 因一处符号错误撤回 3 篇、修订 14 篇、连带更新 13 篇引用、形式化总量记为 300/719 ≈ 42%；10-26 新增 2 篇含形式化稿件（欧氏波方程局部光滑化、以及「The Exponential Time Hypothesis is False」，后者交 Impagliazzo、Paturi、Williams 三人小组复核）；10-29 修 Comparator 命名空间不一致。https://github.com/openai/math/blob/main/history.md
同仓 lean/README.md（本轮读取）。取自此文：单一大型库、建议分块编译；vm.max_map_count 过低时整库编译可能失败的说明与两种规避方式（-DMMAP=OFF、GLIBC_TUNABLES）。https://github.com/openai/math/blob/main/lean/README.md
同仓 lean/ComparatorChallenges/README.md（本轮读取）。取自此文：检查需先安装 comparator、landrun、lean4export，命令形如 lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json。https://github.com/openai/math/blob/main/lean/ComparatorChallenges/README.md

二、检查器的机制与信任假设

leanprover/comparator 仓库 README（本轮读取 master 分支）。以下取自此文：challenge / solution 模块与 permitted_axioms 的 JSON 配置形式；六条成立前提；landrun 沙箱与 systemd-run 对「Linux 7.1 才修」漏洞的额外防护；可选外部内核（external_kernels、nanoda）；「定义洞挑战在缺少额外监督时可被做局」及其 ChallengeSolution := RiemannHypothesis + 反身性做局的例子，与「所有定义洞解答必须由额外（可能是人工的）验证者检查」的规定；项目已在 Lean v4.35.0 并入核心为 lake comparator / lake check。https://github.com/leanprover/comparator

三、独立第三方审计

Ying Xie（Kennesaw State University），《What the Machine Invented: Mining New Mathematical Instruments from OpenAI’s October 2026 Release of AI-Generated Mathematics》，arXiv:2610.17090v1（2026-10-12 提交，math.HO，CC BY 4.0；本轮读取 HTML 全文）。以下取自此文：10-06 首发 722 篇 / 372 族；稿件未经同行评审；抽取阶段未编译任何 Lean 工程；覆盖 38 个族（约占 372 的 10.2%）且偏向知名问题；「抽取不是对源证明的验证」；其计分板记录形式化状态、陈述忠实度、对其它 OpenAI 稿件的依赖与未引用的最近祖先。https://arxiv.org/abs/2610.17090

四、媒体转述（仅作事件与口径记录，未用其数字替代一手）

Quanta Magazine 报道页（本轮读取其更新流，含 2026-10-06《Deluge of 377 OpenAI proofs bewilders the math world》与 2026-10-09《Cracks appear in OpenAI’s wall of proofs》两篇的摘要段）。取自此文：377 个宣称解决的开问题分布在 722 篇稿件；三篇因「放错位置的负号」撤回、剩余 719 篇；约 42% 的 Lean 形式化说法与「少数形式命题存在技术问题」；约 4000 个问题中模型在绝大多数上失败；Johan Commelin（Mathlib Initiative 主任）关于「形式化陈述需要人读 Lean 代码」的表述。https://www.quantamagazine.org/updates/transformation/
Science（AAAS）2026-10-13《OpenAI just changed math forever. Exactly how, no one yet knows》（作者 Tom Howarth）。本文引用其报道中 Olga Holtz（UC Berkeley）关于「被声称的结果 / 被独立验证的结果 / 被理解并吸收进数学文化的结果」三分的表述。⚠️ 该页本轮直接请求返回 403，未取得正文；此句经检索结果摘要与多家转载一致核对，仅作媒体转述引用，未用其任何数字；因未取得正文，此处不列 URL（避免被当成「已打开的可达来源」），读者可凭标题、作者与日期检索原文。

五、本文自行推导（与上述官方数字分列，不可当作官方口径）

「公开结果数 / 尝试问题数」比值 $377/4000\approx9.43\%$ （是比值，不等于每次尝试的成功概率，不可据此反推「每个问题被尝试几次」）；结果侧算力 $377\times3=1131$ Pro-hour，摊到 4000 个问题上得 $1131/4000\approx0.283$ 小时（约 17 分钟，是结果侧算力的比值，不是单次尝试的真实成本，失败尝试同样耗算力）。
假设性算例（非对 OpenAI 做法的描述）：按族数 372 的 Bonferroni 阈值 $\alpha'=0.05/372\approx1.34\times10^{-4}$ ，对应族级假阳性概率 $1-(1-\alpha')^{372}\approx4.88\%$ 。
纯统计示例 $3/38\approx7.9\%$ ：不用于推断这批稿件的缺陷率（该抽取非随机、非独立同分布、且未做逐条缺陷检测，前提不成立）。
平均每族约 1.93 篇（721/373）；已公开撤回占比 $3/722\approx0.41\%$ （分母是首发稿件数；这是下界性质的观察值，不是错误率上界）；未形式化 419 篇（719−300，本文计算，非仓库原文）。
有效保证 $c\cdot f$ 的敏感度示例： $f=1$ 时上限 41.7%， $f=0.9$ 时 37.5%， $f=0.7$ 时 29.2%（本文把 $f$ 取满值 100% 仅作为理论上界，不对本批结果作任何估计）。
第三方审计的族覆盖率 $38/372\approx10.2\%$ （约 10%，本文取整用于叙述），剩余约 89.8% 未覆盖。本文已撤下任何人力/工时外推：该审计由 AI 逐族阅读、未公布工时，折算成「等效全职复核者」缺三个必要参数，算不出可信数字。
假发现率式子中的 $\tau$ 、 $\epsilon$ 为示意参数，非实测值；所列数值只用于说明敏感度，不能当作对本批结果的估计。
误读二里的 58% 是 $1-41.7\%$ 的余数，仅用于说明「未形式化」的规模，不代表「不可信」的比例。
第一节至第九节所有公式与其中的符号定义；版本链哈希式与验收表的层级定义均为本文自建，非任何机构的官方口径。

六、本轮未打开或未获授权的来源（据实说明）

Science（AAAS）2026-10-13 报道在检索结果中可见摘要，但本轮直接请求返回 403（非付费墙提示的纯拦截），未取得正文，故本文未引用其任何数字。