OpenAI 下一代模型 Astra：解出 10 个十年难题，数学研究要被 AI 改写了

8 月 1 日，OpenAI 官方博客发布了一则注定会在数学界和 AI 界同时引发震荡的消息：其下一代模型 Astra 的内部版本，一口气解决了 10 个开放问题——这些问题的核心结果大多已经十年以上没有进展，横跨几何、编码理论、群论、算子代数、量子复杂度、格密码和极值组合学。

这不仅仅是一条"AI 又变强了"的新闻。它把三个严肃的问题摆到了台面上：AI 生成的数学证明可信吗？人类数学家的工作方式会被改变吗？以及——当证明可以被机器验证时，数学这门学科的底层游戏规则，是不是要变了？

这 10 个问题到底有多重

先看分量。据 OpenAI 官方博客，这 10 个问题"主要结果至少十年无进展，多数远不止十年"，且都属于各自领域公认的硬骨头：

1. 非 sofic 群的存在性构造。这是群论的核心开放问题。Sofic 群的概念由 Gromov 在 1999 年提出，直观地说，sofic 群的结构可以用"洗一副有限扑克牌"的方式近似。是否存在非 sofic 群，关系到整个群论研究框架的边界。

2. 反驳 Connes 刚性猜想。算子代数领域几十年的猜想，OpenAI 给出了反例。Connes 猜想研究"某些群能否被其 von Neumann 代数唯一确定"，反例意味着这种唯一性在一般情形下不成立。

3. Erdős 问题 183（多色 Ramsey 数）。Ramsey 数研究的是：给网络链接染若干种颜色，超过一定规模后必然出现三个同色链接构成的三角形。Erdős 问题 183 要求证明多色情形下三角形 Ramsey 数的超级指数下界，这次被解决了。

4. Erdős 问题 146 和 180。极值图论中的紧致性猜想和退化猜想，一并解决。

5. 其他还包括：高维球堆积密度的新上界（逼近 Cohn–Elkies 阈值）、二进制码和球面码的指数级改进、算术电路复杂度下界（永久型计算的算术公式下界达到 n⁴/log n 量级）、一般双人量子博弈的指数级并行重复定理、与后量子密码直接相关的最近向量问题（CVP）的多项式因子不可近似性、Ehrhart 体积猜想（每个维度凸体的最大体积问题）。

注意最后一项——最近向量问题与格密码（后量子密码的核心基础）直接相关。这意味着这次的结果不只是纯数学意义，它可能影响密码学的理论根基。

从"翻车"到"big news"：两次声明的天壤之别

要理解这次发布的分量，必须回顾一年前的事故。

2025 年 10 月，时任 OpenAI 科学副总裁 Kevin Weil 公开声称 GPT-5 解决了 10 个此前未解决的 Erdős 问题。几天之内，维护 erdosproblems.com 的数学家 Thomas Bloom 就揭穿了这个说法——模型实际上是从文献里检索出了已有解法，并不是真的做出了新证明。那一次，OpenAI 在数学界的信誉受到了重创。

2026 年 5 月，情况开始变化。OpenAI 展示了内部模型对 Erdős 单位距离猜想的反例——这是一个 80 年的离散几何难题。这份工作由菲尔兹奖得主 Tim Gowers 参与验证，随后引发了连锁反应：Bloom、Sawin、Schildkraut 和 Zhelezov 基于该反例技术证明了"实数上的 sum-product 猜想为假"（arXiv:2605.28781），Pohoata 等人在 Elekes–Rónyai 问题上取得进展——这些后续成果出现在 OpenAI 官方博客的脚注里。

而这一次，同样的 Thomas Bloom 给出的评价是 “big news”，并认为其分量超过 5 月的单位距离反例。从"被揭穿"到"被认可"，间隔不到一年。

可信度革命：Lean 4 证书把信任从模型手里拿走

这次为什么敢信？关键在验证方式。

OpenAI 发布的不只是论文式的叙述性证明，而是三件套：

• 249 页的手稿合集和模型推理过程叙述
• Lean 4 形式化证明证书，开源在 GitHub（openai/ten-proofs，Apache 2.0 许可）
• 模型对每个证明的思维过程叙述

Lean 是交互式定理证明器，其内核会给出二值判定：证明编译通过，或者不通过。没有中间地带，不需要"信任"模型的能力或诚实——机器会验证每一步逻辑推导。

这恰恰是 2025 年 10 月那次翻车的解药：当时的问题就是"模型声称的证明无法独立验证，后来发现是检索"。而 Lean 证书把"声称"变成了"可检查的代码"。正如 siliconangle 的报道所说：“Lean 证书给了这个公告重量……把对模型的信任从等式中拿掉了。”

2000 美元 vs 数学家的一生

成本数据是最直观的冲击。OpenAI 官方披露：求解这 10 个问题的全部 token，按 Sol API 价格计算大约只需 2000 美元。X 平台上有人专门算了这笔账并惊叹：“OpenAI 花了 2000 美元解决了 10 个击败了人类几十年的问题。”

作为对照，非 sofic 群问题悬而未决了 27 年，Connes 刚性猜想提出更久，Erdős 问题 183 等被列入了著名的问题清单。人类数学史上，任何一个这类问题的解决，都可能成就一位数学家的职业生涯。

当然，这个对比不完全公平——2000 美元只是推理成本，背后的模型训练成本是天文数字。但方向已经清晰：在数学发现这个曾经被认为"AI 永远无法真正参与"的领域，边际成本正在趋近于零。

争议没有消失：四个绕不开的问题

这则公告的质疑声同样值得记录。

第一，公告方式。 Gizmodo 的标题直接批评 OpenAI “把 Astra 的公告偷渡进一篇博客”。Astra 作为"下一代主要模型"，核心能力展示选择了数学证明而非通常的基准测试或产品发布，有人质疑这是为尚未公开发布的模型做公关铺垫。

第二，模型还没公开。 结果是"内部版本"Astra 做的，模型本身没有 API、没有权重、没有演示。数学界无法自行复现"让模型再解一个新问题"的过程。

第三，署名与责任的伦理问题。 OpenAI 在博客中专门回应了数学界的 Leiden 宣言（AI 与数学宣言），表态明确：“数学论证本身由系统生成，人类负责准备手稿和形式化证明，OpenAI 对其正确性负责。” 但"AI 证明是否应该算作人类成果"的争论，不会因为这一纸声明而平息。

第四，评审机制。 十个证明横跨八个领域，即使有 Lean 证书，人类数学家也需要时间理解这些结果的意义、检查是否有隐藏的假设偏差。Bloom 的"big news"是初步判断，学术共同体的正式评审还需要数月甚至数年。

对数学和 AI 行业意味着什么

短期看，这是一次成功的"能力证明"——OpenAI 用可验证的方式展示了 Astra 在长程推理上的恐怖上限，同时为"ChatGPT for Academic Researchers"计划（向 10 万名科学家和数学家免费开放最强模型）做了最好的广告。

中期看，AI 数学可能率先在验证型工作上落地：Lean 形式化、反例搜索、猜想检验、文献检索辅助——这些不需要"灵感"的任务会被 AI 快速接管。OpenAI 5 月反例引发的一系列后续论文，已经证明了这种"AI 开路、人类跟进"的模式是可行的。

长期看，最深刻的改变可能是学科文化层面：当"证明"从不可置疑的人类智力行为，变成"可以被机器验证的形式化对象"，数学共同体对"什么算一个证明"的定义，可能要被重新谈判。

对程序员来说，这件事还有一个更直接的启示：Lean 这类形式化验证工具，正在从学术象牙塔走向实用。当 AI 生成代码越来越普遍，“机器验证代码正确性"的需求只会越来越强——这或许才是这条新闻对开发者最实在的信号。