GPT-6（Astra）破解十年数学难题：AI推理能力的量子跃迁

导语：一份没有参数规模的报告

2026年8月1日，OpenAI发布了一份数学报告。报告里没有GPT-6，没有参数规模，也没有花哨的能力演示，取而代之的是十道长期悬而未决的数学与理论计算机科学难题，每一道都附有Lean 4机器可验证证书。这些结果由一个名为Astra的内部模型生成。报告作者栏写的是Astra，不是任何一位数学家。

这被视为OpenAI下一代主力模型家族Astra的首份成绩单。据多方消息，Astra并非GPT-5.2的迭代补丁，而是与Sol、Terra、Luna并列的全新模型系列，专门负责需要多智能体协同、长时间运行的复杂任务。其最终命名可能是GPT-6，也可能是GPT-5.7，甚至可能直接以”Astra”作为独立品牌——OpenAI内部尚未决定。但一个明确的信息是：跑完这十道难题的token，按Sol API费率折算，总成本仅约2000美元。

这意味着，过去数学家可能要花数年时间撞墙的问题，OpenAI现在用一份云服务账单的钱就能列队扫一遍。这件事的冲击力不在于某个公式有多优美，而在于攻城的成本结构被彻底改写。

一、十道硬骨头：从非sofic群到Connes刚性猜想

OpenAI在报告中列出的不是渐进式优化，而是十几年来几乎无人推动的开放问题，跨度涵盖高维几何、群论、量子复杂性、格密码学、极值组合数学等领域。

最受关注的几项成果

问题	所属领域	历史背景	Astra的突破
非sofic群存在性	群论	Gromov 1999年引入sofic性概念，是否存在非sofic群长期悬而未决	首次构造出非sofic群，给出肯定答案
Connes刚性猜想	冯·诺依曼代数	长期被视为正确的结构性断言	给出反例，直接推翻该猜想
Erdős问题第183号	极值组合数学	多色Ramsey数上界问题长期停滞	给出超指数级下界结果
高维球堆积密度	高维几何	几十年来的关键门槛	将渐近上界推进至Cohn–Elkies阈值
二元码与球面码界	编码理论	任意最小距离条件下的界	提升至指数级更强的水平
permanent复杂度下界	计算复杂性	算术电路计算permanent的硬度	给出n⁴/log n的公式下界

需要指出的是，这些并非”已经彻底定论”的成果，而是证明草稿。但它们的分量在于：每一道都是人类专家至少十年未取得实质进展的公开难题。AI并非在已知框架内做优化，而是在长时间停滞的问题上提供了全新的构造路径与反例。

尤其值得注意的是”否定Connes刚性猜想”这类证伪型成果。构造反例往往比证明定理更难，因为它要求在一片被假定为真的理论疆域中精准找到一个”漏洞”。这暗示Astra的推理能力已不限于演绎链条的延伸，而具备了一定的反向探索与反例搜索能力。

二、Lean 4证书：AI证明第一次有了硬证据

过去两年，AI证明数学题的新闻隔三差五就来一轮，但每次都逃不开同一种质疑：论证看起来漂亮，但到底对不对，没人能验证。这次OpenAI把每一道题的证明都用Lean 4形式化，所有十个成果同步开源到GitHub仓库，附带完整的机器检查证书和推理过程走查。

Lean是一种交互式定理证明器，其内核是一个小而可信的类型论检查器。只要证明能通过Lean内核检查，其逻辑正确性就由数学保证，而非依赖人类审稿人的注意力。下面是一段Lean 4证明结构的示意：

-- Lean 4 形式化证明示意（简化结构）
theorem non_sofic_group_exists :
    ∃ G : Type*, Group G ∧ ¬ SoficGroup G := by
  let G := construct_counterexample
  apply Exists.intro G
  refine ⟨G.group_str, ?_⟩
  -- 以下是Astra生成的核心构造与不可sofic性证明
  exact non_sofic_witness G

这段代码的价值不在于它”看起来像数学”，而在于它可被机器独立验证。Lean验证不能完全替代数学家的同行评议——数学界仍需判断被形式化的命题是否就是他们真正关心的命题——但它至少封死了过去最常见的失败模式：论证链条里藏着一处看起来无害、其实经不起推敲的跳步。换句话说，AI写的证明第一次有了第三方能拿来复查的硬证据。

从自然语言证明到机器可验证证书，Lean形式化并非一步完成，而是一条多阶段流水线。理解这条流水线，才能理解Astra成果的可信度从何而来：

1. 命题形式化：将数学命题用Lean 4的依赖类型论语言精确表述，消除自然语言的歧义。
2. 策略构造：Astra生成一系列Lean tactic（证明策略），逐步填充证明目标。
3. 内核检查：由Lean的小型可信内核对每一步进行类型检查，任何逻辑跳步都会被直接拒绝。
4. 证书输出：通过检查的证明生成可独立复查的机器证书，附推理过程走查一并开源。

论文本身由OpenAI研究员与Astra协作整理。数学论证部分全部来自Astra，OpenAI表示对最终论文的准确性负责，并援引Leiden宣言关于AI与数学署名规范的主张，认为把完全由AI生成的证明归功于人类署名，既低估了系统的贡献，也扭曲了对真正人类智力工作的认知。这一立场本身就具有标志性意义——它意味着学界开始正式承认AI在创造性数学工作中的独立贡献。

三、Astra是什么：长时多智能体协同

把目光从数学成就移到模型本身。Astra是OpenAI正在打造的下一代主力模型家族，核心定位是长时任务——单个任务持续运行数小时甚至数天，内部由多个智能体协同配合解决问题。CEO Sam Altman已在华盛顿向政界人士和监管机构演示过这套系统。

OpenAI首席科学家Jakub Pachocki在去年夏天的官方播客中已预告过这一方向。他当时的判断是：当前系统在长任务上撑不住，OpenAI要的是能在数小时到数天时间跨度上做规划、推理、做实验的模型。配合更长任务的是更大的算力开销——OpenAI的基础设施长期规划正是为这一目标服务。

Astra解决数学难题的过程，正是”长时多智能体协同”的典型场景：它需要在巨大的搜索空间中持续试探、回溯、组合构造，并最终把结果落到Lean可验证的形式化语言里。这远非单次”问-答”所能完成，而是接近一个虚拟研究团队的工作模式。

OpenAI公布的推理能力路线图

时间节点	目标能力
2026年9月	具备研究实习生级别能力的AI系统，能显著加速人类科学家工作
2028年3月	可独立运行研究项目的完全自主AI研究员

Astra很可能就是这条路线上第一步落地的载体。从”研究实习生”到”自主研究员”，其间的跨越不仅是模型规模的提升，更是任务时长、工具使用、自我纠错与协作能力的系统工程。

四、数学界的真实反应

曼彻斯特大学数学家Thomas Bloom在X上把这次结果称为”大新闻”。在评估分量时，他认为这些构造结果的意义大于今年5月发表的单位距离反例。他写道：也许没有证明单位距离猜想的分量那么大，但在构造性结果层面，这是大事件。

Bloom同时反驳了”AI取代数学家”的说法。在他看来，这种说法本身就站不住脚——AI的背后是一个多世纪的数学理论积累，由数学家建造，训练数据是数学家们写下的所有文字。这一观点切中要害：Astra的突破不是凭空而来，而是站在人类数学遗产的肩膀上。

Astra推理技术负责人之一Noam Brown则给出了冷静的补充。他透露OpenAI也尝试过其他重大问题，目前还没有攻下任何一道千禧年难题（Clay数学研究所2000年公布的七道悬赏百万美元难题，二十多年来仅被解开过一道）。Brown承认：”但我们在每道题上花的钱不算多，测试时算力还可以推得更远。”他把Astra定位为科学推理的一次重大跃进。

Brown的话里有两层信息：其一，Astra尚未触及数学的”最高峰”；其二，限制其上限的主要是算力投入，而非方法瓶颈。后者才是最值得重视的信号——如果性能可随测试时算力近似线性提升，那么”花更多钱解更难的题”就成了一条可外推的曲线。

五、对AI发展的启示

这次发布真正的意义，可以从四个维度来理解：

• 成本结构的颠覆：攻克十年悬案的门槛，从”一位数学家数年的职业生涯”变成”一张约2000美元的云服务账单”。这不会立刻取代数学家，但会极大扩展”可被尝试”的问题集合。
• 验证范式的转移：Lean证书让AI证明从”信任问题”变为”可核查问题”。这是AI进入严肃科研的核心前提——可验证性比新颖性更重要。
• 长时推理的兑现：Astra证明了”多智能体+长任务”路线在硬核推理任务上的有效性，为自主科研智能体提供了第一份正样本。
• 署名伦理的破冰：将AI列为证明作者，标志着学界开始正视AI在知识生产中的角色，这对未来的学术评价体系是一次提前的压力测试。

当然，需要保持冷静的是：现阶段Astra仍只是内部模型，对外没有API、没有权重下载、没有可部署镜像。外部数学家尚未充分时间深入审阅这些论据，OpenAI也未披露每道题背后有多少人为的”问题塑形”工作量。如果审阅后多数结论站得住，这次发布将成为AI推理能力的里程碑；如果任何一道最终被推翻，它撤回时的声响也会同样巨大。

结语：从”会聊天”到”会证明”

在Astra之前，大模型的能力叙事长期围绕”会聊天””会写代码””会画图”展开，这些任务的共同特点是容错率高、验证成本低。而数学证明恰恰相反——它容错率为零，验证需要极高的专业门槛。Astra选择在这个最严苛的赛道上交卷，本身就是一种能力宣言。

2000美元解开十道十年悬案，这个数字会被人记住。但比数字更重要的是它背后的趋势线：当推理能力可以随算力外推、当证明可以被机器独立验证、当AI开始以”作者”身份出现在数学论文上，人类与知识生产的关系正在经历一次静默而深刻的重构。数学，曾经被视为人类理性思维最后的堡垒之一，如今正成为检验AI推理上限的试验场。

正如Bloom所言，AI背后是一个多世纪的人类积累。Astra不是数学的终结者，而是数学遗产的一个新继承者——它能否成为真正的合作者，取决于人类如何设计验证、署名与协作的规则。而这些规则，现在就该开始讨论了。