零个 sorry，一个大星号：OpenAI 十项机器验证证明内幕
专栏概述
2026 年 8 月 1 日，OpenAI 发布了一份两年前听起来还像科幻小说的手稿：其下一代模型的未发布内部版本（代号 Astra）为十个搁置了十年或更久的问题生成了完全经机器验证的 Lean 4 证明，涵盖群论、算子代数、球堆积、电路复杂性和拉姆齐理论。这份 249 页的文档附带了一个 GitHub 仓库，其中包含采用 Apache 2.0 许可的证明证书，而每个人都在重复的细节是 Lean 代码中的"sorry"计数为零——这意味着没有任何步骤被留作未证明的占位符，也没有任何漏洞被假设所掩盖。每一行都经过了证明助手的检查，而证明助手不在乎声誉、炒作周期或论文作者是谁。
实际解决了什么
头条结果是显式构造了一个非 sofic 群，解决了 Mikhail Gromov 在 1999 年定义 sofic 性时提出的问题。仅这一项就足以成为人类数学家职业生涯级别的成果。与之并列的还有对 Connes 关于群 von Neumann 代数刚性猜想的反例，这是一个历史上进展以数十年而非数月计的子领域。手稿还报告了高维球堆积的渐近上界改进——这个问题有着奇特公众形象，因为八维和二十四维情形因 Maryna Viazovska 的著名工作而广为人知，而一般高维渐近问题则相对冷门且顽固。其余十项成果还包括电路复杂性和拉姆齐理论方面的额外结果，这两个领域历史上因组合爆炸而使得计算机辅助搜索要么不可行，要么即便可行也缺乏说服力。
这份清单与通常的“AI 解决数学问题”的新闻周期不同之处在于验证层。Lean 不会按曲线评分。一个经 Lean 检查的证明要么能针对形式化陈述编译通过，要么不能，没有审稿人需要讨好，没有导师需要安抚，也没有委员会需要满足。这与“模型生成了专家认为合理的证明草图”是截然不同的说法，后者更接近早期 AI 数学公告的实际内容。
反响分裂
在职数学家们的反应确实存在分歧，而且并非沿着你在典型 AI 炒作故事中预期的那条线。拥有菲尔兹奖且长期对夸大 AI 主张持怀疑态度的 Timothy Gowers 表示，他会毫不犹豫地推荐其中一项证明给顶级期刊——这是来自一位不轻易给出此类认可之人的真实背书。Thomas Bloom 在曼彻斯特大学负责维护 Erdős 问题目录，因此他对“未解决”在实践中的含义有着不亚于任何人的理解，他称这些结果为“重大新闻”。
但热情并非一致，怀疑态度值得认真对待，而非当作条件反射式的守门行为一挥手打发。叶史瓦大学的 Steven Miller 指责 OpenAI 在生成这些结果时实际上借鉴了他自己已发表的研究却未注明出处——这一抱怨与泛泛的“AI 吃了我的内容”的不满不同，因为它来自特定数学社区内部，而该社区数十年来发表的引理和技术正是此类模型所需的确切训练基质。而且时机并非中性：现已获得国际数学联盟背书的《莱顿宣言》早已发出警告，称 AI 公司未经同意利用已发表的数学研究，绕过同行评审，并对该领域长期赖以运行的署名和证明规范施加压力。这一公告恰好落在这场争论的正中央，而非之前。
2000 美元之问
OpenAI 自身的表述大力强调成本：按当前 API 费率，约 2000 美元的计算成本产出了十项证明，而数学界集体花费了超过一百人年也未能解决这些问题。这是一个惊人的数字，而且设计得就是要惊人。但该数字仅涵盖成功运行——它没有说明有多少次尝试未成功，有多少候选证明被生成又丢弃，也没有说明有多少计算投入到了最终未进入手稿的问题上。批评者迅速指出，这使得 2000 美元成为发表成本，而非发现成本。这相当于一家公司只报告其盈利交易：就其所言属实，但如果你想估算该过程的实际经济性，这不是你想要的数字。
还有一个在兴奋中容易被忽视的可复现性难题。OpenAI 外部无人能运行 Astra——它是一个未发布的内部版本，而非已交付产品。因此，证明本身可以独立检查，因为 Lean 是开放的，证书是公开的。但产生这些证明的过程无法被任何其他人独立重复。这是一种不寻常的认知状态：输出层面完全透明，方法层面完全不透明。值得仔细品味这一区别，因为“已验证”和“可复现”在这里承担着不同职责，而将它们混为一谈正是准确新闻稿变成夸大公众叙事的方式。
同样值得注意的是，这一公告没有声称什么。早期 OpenAI 数学公告有时会附带广泛的外部审查或专家全面验证的笼统说法；这一次没有采取这种策略。这里的背书——Gowers、Bloom——读起来更像是个人反应，而非精心策划的审查过程，OpenAI 似乎是在依靠 Lean 的形式化验证来承担可信度工作。这可以说更为诚实，但也意味着社区的的非正式审查——通常通过研讨会、审稿报告和多年试图挑错的过程——尚未针对数学实质内容发生，尽管形式逻辑已经通过了检查。
结合本周其他事件解读
这一切并非发生在真空中。在同样的几天里，OpenAI 将 GPT-5.6“Luna”的价格下调了约 80%，降至每百万输入 token 0.20 美元，据报道 ChatGPT 的周活跃用户数已突破约十亿。欧盟《人工智能法案》的透明度和标签要求也于 8 月 2 日生效。将这些碎片与数学公告放在一起，一个模式便浮现出来：一家公司在消费产品上同时进行价格和规模竞赛，同时试图在最艰难的地形——纯数学——上插旗，在那里“幻觉”不仅令人恼火，而且是一种范畴错误，因为错误的证明根本无法编译通过。
这正是 Lean 验证细节比 2000 美元数字或用户数里程碑更重要的原因。价格战和使用量是可以在任一方向上被操纵的商业指标。形式化证明检查器中的零"sorry"计数则无法以同样方式被操纵——它要么为真，要么仓库无法编译。有趣的张力在于，这一最艰难、最可验证的主张，恰恰也是可复现性最低、包裹在最具争议的署名问题中、并在数学界正围绕《莱顿宣言》组织起来抵制 AI 实验室利用已发表研究的确切时刻到来的主张。Astra 究竟代表着数学发现中真正的阶段变化，还是从一个更大、更混乱的搜索过程中精心挑选出的精彩集锦，这个问题需要未来一年的审视，而非这一份手稿，来回答。