OpenAI 用 2000 美元算力拿下 10 道开放数学——但请先把”自动证明”和”自动发现”分开
8 月 1 日,OpenAI 发布了一份 249 页的论文合订本,内部推理模型 Astra 在 10 道至少 10 年没被解决的开放数学问题上拿到了机器可验证证明。GitHub 仓库以开源许可证发布了对应的 Lean 4 证书——任何研究者都可以下载、编译、自行检查每一步逻辑。
整个过程算力成本约 2,000 美元。
这不是”AI 写了一道数学题”,而是”AI 写了一道数学证明,Lean 编译器能逐行确认它的每一步”。后者与前者的差别,大致相当于”论文有同行评审”与”论文只有作者署名”的差别。
10 道题里最硬的三道
合订本覆盖群论、高维几何、编码理论、量子复杂性、格密码、极值组合等多个领域。难度并不均匀,以下三道最值得拎出来看:
非 sofic 群的首次显式构造。这个概念是 Mikhail Gromov 1999 年提出的悬而未决问题,核心问题是:是否所有有限群都能被有限状态自动机”近似”?Astra 给出第一个显式反例——存在一个群,根本不可能被任何自动机近似。这个构造本身就直接回答了 Gromov 的提问。
Connes 刚性猜想的反例。Connes 在 1980 年代提出一个猜想:具有 property (T) 且 von Neumann 代数相同的群,在代数意义下应当同构。Astra 构造了无穷多对具有 property (T)、共享同一 von Neumann 代数但彼此不同构的群,把猜想推翻。
Cohn-Elkies 线性规划的精确渐近强度。高维球堆积密度的上界自 1978 年起一直由 Cohn、Elkies 等人的线性规划给出。Astra 确定了其精确渐近强度,等于把 1978 年那篇论文从”近似上界”升级到”紧上界”。
其余 7 道同样不是软柿子:算术电路复杂性下界 n^4/log n、量子并行重复定理的指数下界、欧几里得最近向量问题的多项式硬度、多色三角形 Ramsey 数的超指数下界,以及 Erdős 问题 #146 与 #180 的解决——后两题来自 Erdős 留下的极值图论公开问题集。
5 月那一次,是这次的前戏
把时间拨回 5 月,Astra 模型家族的同一支刚刚推翻了 Erdős 单位距离猜想——1946 年提出,80 年没人能给出反证。Astra 用几何与复数系统的组合,证明存在无穷多个 n 使单位距离对数比 n 多一个 δ > 0 的指数增量,把 Erdős 当年的乐观上限直接打成不成立。
Fields 奖得主 Tim Gowers 当时公开表示,这份证明换他来评审会毫不犹豫地推荐到顶刊数学期刊发表。9 位数学家(其中包括 Gowers 与 Noga Alon)随后联名发了一篇伴随论文,把证明改写成人类数学家更易读的形式。
Erdős 问题目录维护者 Thomas Bloom 把 8 月的 10 道题评价为”big news”,且”比 5 月的单位距离成果更重大”。
为什么”Lean 证书”是这件事的真正门槛
过去两年,AI 在数学上的成绩几乎都被同一类问题反复追问:”你确定它真的证明了对吗?”答案通常是:模型自己说对了,但我们没有独立方式核实。
Astra 的 10 道题里,所有论证都先被转写成 Lean 4 形式化代码——一个数学步骤如果逻辑链不能自洽,Lean 编译器直接拒绝;通过了,意味着整个论证链条在形式逻辑上无懈可击。研究者不需要”相信 OpenAI”,只需要”相信 Lean 编译器”,而后者是数学界广泛接受的开源工具。
这件事的边界意义比”AI 解题”更大:从此 AI 给出的数学结果,不再是”观点”,而是”可独立验证的事实”。机器验证与人类验证可以并行,大大压缩”从结论到共识”的延迟。
别把”自动证明”误读成”自动发现”
一些媒体把这件事描述成”AI 自主发现新数学”,但这个表述会掩盖一个关键事实:Astra 模型本身不向外部研究者开放。题目选择由 OpenAI 控制;研究人员在事后介入审查、改写论文;机器验证的也只是被形式化的那部分论证,而不是模型”为什么选择这个证明路径”。
OpenAI 研究员 Noam Brown 自评很冷静:”Sadly, no Millennium Prize Problems (yet)。”2,000 美元的算力成本对应的是”成功发表的结果”,而不是”全部实验开销”——失败的尝试、模型探索的弯路、形式化过程中的人工干预,都没有计入。
AI 评论员 Gary Marcus 评价这次发布”impressive but substantially oversold”(令人印象深刻但明显被高估)。一些数学家私下指出,10 道题里可能有相当一部分是”技术上可以接近、只是此前没有得到足够关注”的问题,真正的”反直觉突破”可能只占一部分。
接下来 12 个月,该看什么
短期看,有三个观察点:
1. 独立复现。Astra 模型本身不公开,独立研究者能不能用别的模型(Claude、DeepSeek、Qwen)复现同等水平的证明?如果能,说明这是方法论的胜利;如果只有 OpenAI 内部能做到,那就是工程能力的胜利,而不是科学方法的胜利。 2. 形式化生态扩张。如果其他 AI 研究机构(Anthropic、Google DeepMind、xAI)都开始用 Lean 形式化发布数学成果,这套”机器可验证”的工作流就会从 OpenAI 内部规范升级为社区共识。 3. 真正的”AI 发现”案例。下一步值得追问的不是”Astra 又解了哪道题”,而是”Astra 是否提出过一道人类没问过、但解出来有意义的新问题”——后者才是 AI for Science 的下一个分水岭。
2026 年中,Anthropic 与 Google DeepMind 都在数学形式化上加大投入。DeepMind 的 AlphaProof 已经在 IMO 风格的题目上拿到了金牌级表现;AlphaEvolve 8 月 21 日把 Stetter 猜想相关常数 ω 推到 2.371177。OpenAI Astra 的 10 道题真正改变的不是”AI 会数学”,而是”AI 给出的数学结果从此可以被任何研究者独立验证”。
参考来源:OpenAI 8 月 1 公告、Tim Gowers 与 Noga Alon 等 9 人伴随论文、Thomas Bloom Erdős 问题目录评价、Fields Medalist 与 Noam Brown 评论、Wortins/CySecurity News 多源核验。