OpenAI Astra 数学成果：从模型输出到可验证代码

OpenAI 于 8 月 1 日公布了十项其声称在数学和理论计算机科学领域取得的新进展。这些成果由其下一代主力模型 Astra 的内部版本生成，随后在人工协助下整理成论文，并被形式化为 Lean 证书。

最后这句话才是整件事的关键。

最吸引眼球的标题当然是某个模型“会做数学了”。这么说也没错，但这个表述太模糊，没什么实际意义。真正值得关注的，是工作方式上的转变。OpenAI 发布的不只是一个 benchmark 分数，也不是一张看起来像证明答案的截图，而是可供外部人员审查的论文、Lean 文件，以及带有解说的推理过程记录。

这才更接近严肃的 AI 研究辅助工具未来应有的工作方式。

声明很重磅，但成果的交付方式更重要

OpenAI 表示，Astra 在数学和理论计算机科学的多个问题上得出了新结果，涉及非 sofic 群、球体堆积、编码理论、下界、Ramsey 数、量子并行重复，以及该领域其他高度专业的方向。配套的 GitHub 仓库包含这十项成果的 Lean 形式化证明。

我并不是这些细分领域的一线数学研究者，所以不会假装自己能够裁定每项证明的新颖性或重要性。而这恰恰就是问题所在。面对一个声称解决了高难度开放问题的方案，我们大多数人都无法仅凭阅读判断：它所证明的目标命题是否正确，结果是否具有实质性创新，或者某个隐藏条件是否悄悄改变了原问题的目标。

Lean 证书确实有帮助，但它无法神奇地解决证明评审中涉及社会共识的部分。它可以检查：在证明助手内部，根据给定的定义，某个形式化命题是否能够成立。但仅凭它本身，你无法判断这个形式化命题是否就是所有人真正关心的那个非形式化问题，也无法判断该成果是否配得上标题中的重磅说法。

因此，这里真正有用的单位不是“AI 答案”，而是一套可供评审的材料包。

这套材料包分为多个层次。

首先是模型生成的搜索过程，它找到了一个候选论证；然后是由人类整理的论文稿件，供专业人士阅读；接着是 Lean 形式化证明，用来检查机械化、精确定义后的版本；此外还有对模型搜索过程的叙述记录——它可能有用，也可能没用，但至少为评审者提供了一份材料，可以与最终润色后的证明进行对照。

这比一段以“所以问题已解决”收尾的聊天机器人对话要强得多。

这种模式同样适用于数学之外的 Agent

开发者其实早已在面对同一种问题，只不过它的表现形式没那么光鲜。

一个 Agent 提交了 PR。代码可以编译。解释听起来合情合理。如果运气不错，测试也能通过。但真正的问题并不是 Agent 是否生成了一些看起来像工作成果的文本，而是它有没有留下足够的证据，让人类无需从头重做一遍，就能完成对这些工作的审查。

一个真正有用的编程 Agent 不应该只说“已修复”。它还应该留下代码 diff、修改前会失败的测试、修改后通过的测试、它所做的假设、它刻意没有修改的文件，以及在判断错误时可以采用的回滚方案。

一个真正有用的数据 Agent 不应该只说“数据集已清理”。它还应该留下 schema diff、被丢弃的行数、异常值处理规则、处理前后的示例行，以及生成最终数据表所使用的查询。

一个真正有用的研究 Agent 不应该只提供摘要。它还应该留下来源链接、引用范围、存在分歧的观点，以及它无法验证的声明。

数学让这个问题显得格外刺眼，因为证明的门槛很高。软件领域之所以让人觉得标准更宽松，只是因为我们早已习惯了糟糕透顶的审计轨迹。

2,000 美元不是最值得盯着看的数字

OpenAI 表示，找到这些问题的解法所需的 token 总量，如果按照 Sol API 的费率计算，成本大约为 2,000 美元。这个数字肯定会被到处引用，因为相对于其声称取得的成果，它既清晰明确，又小得出奇。

但我会谨慎看待这个数字。

Token 成本并不等于项目成本。它没有包括选择尝试哪些问题的成本、未被纳入公开路径的失败尝试、人工评审、论文稿件整理、形式化工作，以及围绕“哪些内容可以安全公开”这一决策所需的整套机构运作。也许内部核算完全公平，也许并非如此。无论是哪一种情况，这个数字都没有它所代表的趋势重要。

这个趋势就是：前沿模型的能力正在变得足够强，以至于瓶颈开始从生成转移到验证。

这并不是一个微不足道的变化。它意味着，稀缺能力将不再只是“我能不能让模型生成一些令人惊叹的东西”，而更多是“我能不能构建一套工作流，让那些看起来令人惊叹的输出都附带可核验的凭证”。

看似无聊的未来，才是真正有用的未来

许多 AI 演示都围绕揭晓结果的那一刻进行优化。模型写出一个程序，模型解开一道谜题，模型找到一个证明。所有人都盯着最终产物。

但我通常更信任那些看起来无聊得多的部分。我能否检查它的运行过程？能否重新执行验证？持怀疑态度的人能否攻击其中最薄弱的环节？系统能否区分它真正知道的内容与它仅仅猜测的内容？

这正是 Lean 文件的重要之处。不是因为形式化方法突然拥有了魔法，也不是因为每个领域都可以变成 Lean。它们之所以重要，是因为它们揭示了一套严肃工作流应有的形态：模型提出方案，系统记录过程，人类进行审查，机器检查捕获某一类错误，剩余的判断则继续交给真正理解该领域的人。

这听起来没有“AI 解决了数学问题”那么激动人心。

很好。兴奋感不值钱。审计轨迹才是那部分真正有可能经受住实际工作检验的东西。

对于 Agent，这就是我想借鉴的经验。不要问模型能不能给出答案。假设它总能生成某种“看起来像答案”的东西，然后再问：它留下了哪些证据？

真正有用的系统与魔术把戏之间的分界线，就在这里。

如需采取进一步措施，你可以考虑屏蔽此人和/或举报滥用行为。