证明变绿，不等于验证链已经走完

8 月 1 日，OpenAI 发布了十项数学和理论计算机科学成果。每项成果都附有论文、推理过程说明和 Lean 证书。同一天，Lean 的创始人发布了一份事故复盘：一篇由 AI 辅助生成、没有使用 sorry 的 Collatz 猜想“反证”，此前竟同时通过了 Lean 官方 kernel 和一个旧版独立检查器。原因并不是同一处代码被复用，而是两个实现里恰好各有一个不同的 bug。

这两件事并不互相抵消。Collatz 事件不能证明形式化验证没有价值；十份新证书也不能证明独立学术审查已经结束。把两者放在一起，更值得产品团队记住的结论是：证书是一项可执行的主张，而它代表什么，取决于接受它的整条验证器供应链。

这不只是数学团队的问题。小团队收到的 AI 产物越来越常带着一个绿色信号：schema 校验通过、策略检查通过、出处记录签名有效、测试全绿、静态分析无报错，或者自动审计已完成。绿色信号很有用，但它不会自动解释自己。团队仍要知道：实际运行的是哪个 artifact、哪个检查器、加载了哪些依赖；所谓独立路径到底独立在哪里；已知坏输入能否被拒绝；检查器打补丁以后，旧证书怎么处理。

真正的产品风险，往往出现在绿色信号开始授权下一个不可逆动作时：公开发布一项主张、移动资金、迁移数据，或者取消人工复核。

为写这份现场笔记，我把 OpenAI 的 ten-proofs 公共仓库固定在 commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6，检查了工具链和依赖锁；随后在隔离的临时目录中安装仓库指定的 Lean 4.32.0，下载 mathlib 缓存，并成功构建 MulticolorTriangleRamsey target。Lake 最终报告完成 8,656 个 job，构建前共取回 8,639 个缓存文件。

这只是一次原生路径重放，不是独立验证。本次环境是 macOS，而 Comparator 文档列出的可信运行环境依赖 Linux sandbox 工具 landrun，因此我没有运行 Comparator。正确的凭证状态应写成“原生重放通过；独立检查器未运行”，而不能写成“证明已获独立验证”。这个差别，正是下文演练要保留下来的东西。

两个发布事件，其实在追问同一个信任问题

OpenAI 表示，内部 Astra 模型为十个长期未解问题生成了数学论证，覆盖几何、编码理论、群论、复杂性、密码学和组合数学；随后由人类与同一模型整理成论文，再由模型把每项论证形式化成 Lean 证书。OpenAI 还表示会对正确性负责，并邀请数学界进一步检查这些结果（官方发布）。这些都是重要且可检查的产物，但不能据此推断十项成果都已经完成独立同行评议。

公开证书仓库的价值在于，它不只提供 PDF。仓库锁定了 Lean 4.32.0，在 lake-manifest.json 中记录精确依赖 revision，在 formalization.yaml 中列出主声明、允许使用的公理和对应 Comparator 配置，还提供了独立检查所需的 challenge。manifest 对列出的主结果报告 sorry_count: 0。这让成果具备了可检查性。

Lean 事故给出了必要的证据边界。Leonardo de Moura 的官方复盘说明，7 月 25 日发布的 AI 辅助 Collatz “反证”利用了 nested inductive type 中 phantom parameter 的 kernel 实现 bug。7 月 28 日，问题被缩减成一份 False 的证明，issue #14576 随即建立，大约一小时后修复就已推送。普通 frontend 会挡住这个类型错误，但直接通过 metaprogramming 发送声明可以触达有缺陷的 kernel 路径。

同一个 artifact 还通过了一个旧版 nanoda。复盘指出，nanoda 的问题来自另一个 projection type name 检查 bug，并且在 Lean bug 被报告前已经修复。也就是说，这不是“一套共享代码同时出错”，而是两个实现缺陷与版本过期罕见地组合到了一起。

因此，产品团队不必争论“形式化验证到底可信不可信”。更精确的问题是：

一项机器可检查的 artifact，要具备哪些证据，才能从“在某处被接受过”升级为“我们可以解释、可以追责、也可以撤销的发布证据”？

不要只留一个绿色勾；至少区分五种状态

很多团队会把每条成功命令都压缩成 verified=true。这个布尔值会抹掉最重要的差别。建议保留五个状态：

OpenAI 仓库在交付时已经达到质量较高的“已锁定”状态。本次现场重放让其中一个 target 达到“原生重放通过”。由于没有在本地运行独立路径，它没有达到“交叉检查通过”。即使证书可以构建，十项数学成果本身仍需要领域专家继续判断。

这套词汇还能避免两种常见误判。第一，构建失败不一定推翻主张；它可能只说明依赖缺失、平台不兼容或凭证不完整。第二，构建成功也不能证明 formal statement 与读者理解的自然语言主张完全一致。检查器能证明“某个形式系统接受了某个声明”，不能自动证明新颖性、归属、实用性或现实适用性。

先建立验证器 SBOM，再执行检查

软件物料清单用来记录产品组件；验证器 SBOM 用来记录究竟是哪些组件赋予了证书“被接受”的含义。

最少应保存以下字段：

verification_receipt:
  claim_id: "multicolor-ramsey-main-result"
  artifact_repo: "https://github.com/openai/ten-proofs"
  artifact_commit: "94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6"
  target: "MulticolorTriangleRamsey"
  statement_id: "ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit"
  native_checker: "leanprover/lean4:v4.32.0"
  dependency_lock: "lake-manifest.json sha256:<record-at-run>"
  permitted_axioms:
    - "propext"
    - "Classical.choice"
    - "Quot.sound"
  native_replay:
    status: "pass"
    platform: "macOS arm64"
    command: "lake build MulticolorTriangleRamsey"
    jobs_completed: 8656
  independent_check:
    status: "not_run"
    reason: "documented landrun/Linux sandbox unavailable in this environment"
  known_bad_suite:
    status: "not_run"
  domain_review:
    status: "not_assessed"
  decision: "hold_at_native_replay"

不要把上面的观测值复制到另一场运行里。artifact hash、manifest hash、平台、命令和结果都必须重新计算。可以复用的是 schema，不是证据。

仓库中的 formalization.yaml 是一个很好的起点，因为它把人类可读的成果映射到 Lean declaration、文件、公理和 Comparator 配置。lockfile 则把 mathlib、Comparator、lean4export 和 Lean4Checker 等依赖固定到明确 revision。真正有用的凭证要连接这两个层面：究竟检查了什么主张，以及什么软件解释了这份证书。

重放原生路径，但不要夸大结果

原生路径重放回答的是一个基础却必要的问题：团队能否根据公开材料，重新建立生产者原本预期的接受路径？

本次运行使用隔离临时目录和临时 ELAN_HOME。流程包括检出固定 commit、安装声明的 Lean 4.32.0、执行 lake exe cache get，再执行：

lake build MulticolorTriangleRamsey

构建成功。但它不能被扩写为“十项证明已获独立确认”。我只选了一个 target，只使用标准 Lean 路径，没有执行 Comparator challenge，也没有进行数学新颖性审查。依赖来自配置的 mathlib cache；revision 已锁定，但本次运行并没有为每个缓存对象另行建立签名供应链出处。

这些限制不是应该藏在脚注里的杂音，它们直接决定状态。合格的构建日志应包含：

• 不可变的 artifact revision；
• 验证器版本与 binary 来源；
• dependency lock 与 cache 来源；
• 平台和架构；
• 精确命令与退出状态；
• 覆盖了哪些 target；
• 开始和完成时间；
• 准备与检查阶段的网络访问；
• warning、跳过步骤和 reviewer 身份。

如果必须做一处未记录修改才能构建，就把 patch 当成新的输入。如果 default branch 已经移动，不要悄悄跟随。如果决定信任 cache，就把这个判断写出来。可复现不是“不需要判断”，而是把判断保存成可以审计的输入。

独立路径必须证明自己独立在哪里

“我们用了第二个检查器”还不够。两条命令可能共享同一个 parser、导出表示、library cache、kernel 逻辑，甚至同一种 bug。

Lean 的 Comparator 会检查 solution 中的指定 theorem 是否与 challenge statement 一致、是否只使用允许的公理，以及能否被 Lean kernel 接受；它还可以启用 nanoda。README 也明确列出了可信计算基：操作系统、硬件、sandbox、Lean 安装、landrun、lean4export，以及某些情况下预先构建的 cache。把这些依赖公开出来是一项优点，因为团队因此能检查“独立”究竟是真是假。

为每条第二路径记录四种距离：

Lean 事故说明，独立性必须和版本新鲜度一起记录。de Moura 的复盘指出，Collatz artifact 通过的是一周前的 nanoda，而相关 nanoda bug 当时其实已经修复。过期检查器依然可能是独立实现，但它的判断并不代表团队以为自己正在依赖的版本。

本次 macOS 重放在这一关停下。为了挽救一个绿色标签而安装未经说明的替代 sandbox，或者把普通原生构建改称“独立”，都会改变方法。正确下一步是在兼容、隔离的 Linux 环境中调度仓库已经发布的 Comparator challenge，并把结果附到同一份凭证里。

用已知坏样本集反过来测试验证器

正向 fixture 能证明检查器接受预期输入，却不能证明它会拒绝团队真正担心的失败。因此，每条证书流水线都需要一套已知坏样本集。

Lean Kernel Arena 提供了合适的运行模型：把预期应该接受、拒绝或主动放弃的 artifact 同时交给多个 checker，并公开结果矩阵。它跟踪 checker revision、正确接受覆盖、面向 soundness 的拒绝结果、运行时间和内存。官方复盘还说明，#14576 以及相关 non-uniform parameter 案例已经进入 Arena regression。

对非数学产品来说，已知坏样本可以包括：

• 签名后又被修改 payload 的记录；
• schema 合法、但货币或单位在语义上无效的对象；
• 使用过期规则包做出的策略判断；
• 指向另一个 commit 的测试报告；
• 使用了“允许但不符合预期”的公理或例外的证书；
• 输出本身有效，但依赖 manifest 缺失；
• 从历史生产事故中缩减出来的单个确定性 fixture。

每当 verifier、exporter、sandbox、依赖解析器或 cache policy 改变，都应重跑这套样本。第二个检查器也应拒绝相同的危险 artifact，而且团队要能解释它为什么拒绝。只有好输入上的一致，没有坏输入上的分歧测试，很容易制造虚假的多样性。

把补丁与撤销演练纳入发布流程

检查器缺陷仍然是软件缺陷，只是它们控制的标签后果更大。发布流程必须提前回答：补丁出现以后怎么办？

Lean 的第一份修复 PR #14577补上缺失的参数检查，并于 7 月 28 日合并；随后 PR #14582进一步强化 nested inductive parameter 的 uniformity 检查。公开响应还包括 patch release、regression case、额外 hardening，以及每天跟踪 nanoda，让 Comparator 和 lean-eval 不会继续依赖过期 checker。

不要等事故发生，再第一次尝试撤销。演练应覆盖：

1. 标记受影响的 verifier 版本范围和证书集合。
2. 停止由这些版本发出新的“已验证”标签。
3. 在修补后的 checker 上先跑已知坏样本集。
4. 重新检查已经准入的证书，并从影响最大的主张开始。
5. 比较修补前后的结果，同时保留两份日志。
6. 对无法通过新版本的主张降级或撤销。
7. 通知依赖这些结论做决策的人，而不只通知 verifier 维护者。
8. 用补丁 revision 和剩余未知项签发新凭证。

许多“证书产品”到了这里就退化成了 badge 系统：可以发绿标，却查不出哪些绿标依赖有缺陷的 verifier。能否撤销不是额外的事故响应能力，而是验证本身的一部分。

把检查器接受与主张审查分开

形式系统接受回答的是一个精确问题：在这些假设和实现下，这条 declaration 能否通过？产品决策通常还需要其他答案。

对 AI 生成的研究成果，领域专家仍要检查 formal statement 是否准确表达论文声称的 theorem、假设是否合理、前人工作是否获得归属、成果是否新颖或有用。OpenAI 明确邀请数学界把十项成果放入领域语境。仓库 manifest 中记录的 agent-reviewed，也不应被改写成外部同行评议。

对 AI 构建的产品，类似缺口很常见。通过 JSON schema 不代表退款公平；通过安全策略不代表策略覆盖了新工具；unit test 全绿不代表用户能从一半完成的副作用中恢复；出处检查通过也不等于内容真实。

因此，凭证要分开记录：

• 语法有效性；
• 检查器接受状态；
• 独立检查状态；
• 语义或领域审查；
• 运行场景测试；
• 发布决定；
• 撤销状态。

一次机器成功不能把其他未知字段全部覆盖成“通过”。

这套演练要捕捉的失败模式

工具链漂移。 artifact 今天能通过，只是因为 verifier 或依赖图悄悄改变。应锁定 release，并保存实际解析出的 revision。

过期的独立性。 第二检查器架构独立，却错过相关上游修复。要记录 commit、发布日期和已知 issue 状态。

共享盲区。 两条路径消费同一份格式错误的 export、cache 或中间表示。应明确共享组件，并尽可能增加绕开它们的检查路径。

只有正向测试。 所有 fixture 都是“预期通过”。应维护缩减后的负向样本；一旦预期拒绝变成接受，pipeline 必须失败。

statement 漂移。 证书证明的是一个相近 formal statement，产品或论文却声称了更宽的结论。要把自然语言主张绑定到稳定 statement ID，并要求领域审查。

badge 永久存活。 verifier bug 修复了，但旧绿标无法按受影响版本查询。每份凭证必须保存 verifier 身份，并定期演练撤销。

平台补救被伪装成等价运行。 缺依赖或不支持 sandbox 时，团队私下换了一条路径，最后却按原方法报告。正确做法是记录 not_run，或者把新方法作为独立证据保存。

哪些场景适用，哪些不适用

当 AI 生成 artifact 将用于支撑高影响决定，而且确定性或形式化 checker 是证据的一部分时，适合使用这套演练。例如研究主张、策略引擎、自动生成的数据迁移、密码学出处、安全论证、财务转换或受监管报告。

不必把完整流程强加给每一段低风险草稿、UI 文案建议或一次性 prototype。错误绿标的后果越高，验证成本才应越高。普通应用代码往往可以采用精简版：固定 commit、干净构建、负向测试、独立 review 和 rollback 链接。

这套协议也不能证明两个实现绝对独立、formal model 与现实完全一致，或者未来永远不会出现新 bug。已知坏样本只覆盖已知类别；原生重放只覆盖一个环境；第二 checker 只能降低一部分相关风险；专家复核补充的是判断。它们都不能把不确定性降成零。

一套 48 小时验证器供应链演练

第 0–4 小时：盘点。 选一份会影响重要决定的 AI 生成证书，冻结 artifact revision，记录自然语言主张、formal statement 或 policy ID、verifier 版本、依赖、cache、平台和负责人。

第 4–12 小时：原生重放。 在隔离环境中重建预期路径，保存命令、日志、退出状态和偏差。失败后先分类原因，不要先修改输入。

第 12–20 小时：负向样本。 至少加入三个已知坏 artifact，其中一个来自历史失败的最小复现，一个代表 stale version，确认原生路径会拒绝它们。

第 20–32 小时：独立路径。 运行由另一方维护的 checker，或者使用独立实现的校验路径。记录共享依赖和版本新鲜度。如果环境不兼容，就写 not_run，再调度正确环境。

第 32–40 小时：补丁模拟。 假设主 verifier 版本受影响，查询证书集合、暂停新标签、重跑一份已准入 artifact，并实际生成一份撤销通知。

第 40–48 小时：决策。 只签署四种状态之一：hold_at_received、hold_at_native_replay、cross_checked_pending_domain_review 或 approved_for_bounded_use。同时写明谁可以重开决策，以及需要新增什么证据。

这套演练不是为了让团队怀疑每一张证书，而是为了让每一次信任升级都可观察。OpenAI 的十份证明说明，生产者可以公开多么丰富的可检查材料；Lean 的快速事故响应则说明，checker 版本、负向测试和补丁传播仍然属于主张的一部分。小团队应同时借用这两个习惯：发布 artifact，也发布它的绿灯在什么条件下才有资格继续亮着。

参考资料

1. OpenAI：Ten advances in mathematics and theoretical computer science
2. OpenAI：ten-proofs Lean 证书仓库
3. OpenAI：本次检查 commit 的 formalization.yaml
4. Leonardo de Moura：Kernel Soundness Bug #14576 复盘
5. Lean 4：Issue #14576，kernel 接受错误结构 projection
6. Lean 4：PR #14577，补上 kernel inductive declaration 检查
7. Lean 4：PR #14582，检查 nested inductive parameter uniformity
8. Lean Kernel Arena
9. Lean Comparator
10. Leonardo de Moura：Who Watches the Provers?
11. nanoda 独立 Lean 检查器
12. lean4lean 外部检查器与 Lean 元理论形式化