AI证明可验证了：OpenAI开源Lean 4形式化验证工作流

本月早些时候，OpenAI 宣布其尚未发布的 Astra 模型解决了十个开放数学问题，我差点就滑过去了。"大模型做出了惊人的事情"在这种时代已经是背景噪音，何况我也无法评估一个关于非 Sofic 群的结果。我猜大多数一线开发者都和我一样。

让我停下来的是后面一个细节：这次结果没有以论文和新闻稿的形式发布。他们发布的是一份 249 页的手稿，外加 Lean 4 证明证书，放在 GitHub 上，采用 Apache 2.0 许可证。而且这个仓库的 sorry 计数是零。

这个细节在我脑子里转了两周了，因为我认为它描述了一种我们其他人最终会使用的流程——不是用于数学，而是用于普通代码。

零 sorry 意味着什么

如果你没用过 Lean：它是一个证明助手，而 sorry 是它的关键字，表示"相信我，我稍后会证明这部分"。它是形式数学中的 TODO。一个没有任何 sorry 的 Lean 开发意味着每个证明的每个逻辑步骤都已经被内核机械地检查过了。不需要审稿人的耐心，也不需要"我选择相信你"。

这就改变了这个公告的性质。没人必须相信 OpenAI 关于其模型的声明。你可以克隆这个仓库并在你自己的笔记本上运行检查器，数学家们现在正在这样做。Astra 是否"理解"冯·诺依曼代数是一个哲学问题。证明是否有效是一个构建命令。

我本人还没有运行过检查器——这在我的待办清单上，我运行后会在这里添加更新。但这件事的形态才是我感兴趣的，而这个形态不取决于我的笔记本。

生成现在很便宜；验证才是产品

阻碍人们信任 LLM 输出的问题一直是：检查它所需的成本几乎和你自己做这项工作一样高。审查五百行生成的代码并不明显比你自己写它们更快。这就是为什么"模型写的"仍然让人们紧张，而且它应该紧张。

Astra 的发布颠覆了这道算术题。OpenAI 估计找到所有十个解决方案的计算成本约为 2000 美元——这意味着这个工作流几乎肯定是一个巨大的并行搜索，Lean 内核过滤掉了每一个错误的尝试，大部分钱都花在了被丢弃的候选方案上。生成一个证明需要前沿规模的搜索。检查它只需要几分钟，而且检查器不会产生幻觉。

昂贵的、易错的步骤和便宜的、可靠的步骤被分开了。这就是整个诀窍，而且它不是数学特有的诀窍。我们已经生活在一个较弱版本中：类型、测试、CI。新闻是模型现在已经足够好，可以满足比我们目前指向它们的更严格的检查器。

我从中学到了什么

自从阅读了这个之后，我一直在问我自己的每一个 LLM 生成产物一个问题：什么是最便宜的确定性检查，能够在这里抓住一个谎言？有时候答案是类型签名。有时候是生成的代码必须通过的基于属性的测试。很少是"一个人仔细阅读它"，这是我之前隐含依赖的检查。

值得一提的是，克莱数学千年问题一个都没有被攻克，OpenAI 自己的表述也承认了这一点。这不是"数学家们要失业了"。它更窄，也更有用：生成许多候选方案，机械地验证，保留存活者——而且你的检查器的质量比你的生成器的质量更重要。

如果你已经在用比单元测试更严格的东西运行生成的代码，我真的很想听听进展如何。