真正的突破不只是十项成果，而是可验证的研究
OpenAI 这次数学发布的意义，不只在于“解出了多少题”，更在于它展示了一种随成果一并交付可检查、部分可机器验证证据的 AI 研究范式。
OpenAI 在 8 月 1 日发布了十项横跨球体堆积、编码理论、群论、复杂性、量子博弈、格问题和极值组合学的成果。初版手稿共 249 页，8 月 6 日更新版增至 253 页，两版目前均可公开访问。论文称这些结果由 OpenAI 的内部模型取得。12
最吸引眼球的说法当然是：AI 一次攻下了十个长期问题。但真正影响更深的变化藏在交付方式里——这次公开的不是一组需要读者照单全收的答案，而是一套验证栈。外部研究者可以逐层查看数学论文、由模型撰写的思路复盘、Lean 4 形式化代码，以及用独立内核复查导出证明的配置。346
| 层级 | 公开材料 | 有助于检查什么 | 仍不能解决什么 |
|---|---|---|---|
| 数学论证 | 249 页论文 | 定义、引理与证明结构 | 学术重要性与同行评审共识 |
| 过程复盘 | 推理过程文档 | 所声称的弯路、障碍与视角转换 | 原始提示词、完整推理轨迹及全部失败尝试 |
| 形式化证书 | Lean 4 代码库 | 编码后的结论能否在 Lean 中推出；项目元数据称主要结果没有 `sorry` 占位符 | 形式化表述是否与每一项原始数学主张完全一致 |
| 独立重放 | Comparator 检查配置c6 | 在 Lean 主内核之外复查导出的声明 | 更广泛的数学解释 |
这个区别很关键。写得漂亮的证明仍可能藏有细小错误；形式化证明也可能严密地证明了一个“写错的问题”。代码库将当前评审状态标为“agent-reviewed”，而不是同行评审；推理复盘文档也明确说明，它是模型在读取原始思维链和成稿后进行的回溯式重建。45 换句话说，这次发布显著提高了可审计性，但没有取消专家判断的必要。
对 Digital AGI 而言，结论不是“数学已经可以一键完成”，而是前沿系统开始将论文、形式化代码和可重放的检查配置一并公开。下一代真正有用的评测，应继续追问：提示词和搜索过程是否公开？外部团队能否重放形式化证书？核对非形式化定理与形式化表述之间的一致性，需要多少专家时间？能让这些成本变得可见的系统，比只公布更多“胜利数字”的系统更有科学价值。