2000美元，10道悬而未决的数学难题，一个会“想”好几天的AI

未分类

2026年8月1日，OpenAI干了一件让数学界和AI圈同时震动的事。

他们发布了一个叫Astra的内部模型，一口气解决了十道长期悬而未决的数学难题——最老的一道已经卡了人类快50年。全部证明以Lean 4代码形式开源在GitHub，任何人都能下载验证。而完成这一切的推理成本，按API费率换算，大概只有2000美元。

是的，2000美元。平均每题200美元。

这事太大了。大到Sam Altman在发布前密集拜会了多位参议员、财政部长和商务部长，大到白宫刚签发的AI审查行政令可能首先就要用在这个模型上，大到陶哲轩在国际数学家大会上说“数学界迎来百年新危机”，大到Hinton预言未来十到二十年AI可能创造出人类无法理解的新数学。

但对我们普通人来说，这件事最让人好奇的问题其实很简单：一个本质上是“文字接龙机器”的AI，怎么可能做数学证明这种不能错一步的事？

答案藏在Astra的设计里。

Astra的核心特征是多智能体长时间协作。它不是一个大模型在单打独斗，而是一个根智能体创建多个子智能体，各自分头探索，互相验证纠偏，最后汇总结果。这个过程可以跑几个小时甚至几天。

为什么要这么设计？这得回到大模型的底层原理。所有大语言模型本质上都是概率预测网络——给定上文猜下文，一个词一个词地往外蹦。它们没有真正的逻辑推理能力，只有从海量数据中学会的“逻辑模式”。就像一个人看了无数篇数学论文后，能模仿出推理的腔调和步骤，但并不真正理解自己在说什么。

这种“推理”就像一团概率云，在简单的逻辑地带能紧紧包裹住正确的推理链，但在复杂的边界条件、反直觉的抽象地带，这团云可能就飘走了。模型会自信地输出一段形式上像证明、但某一步偷偷用了未声明的假设或忽略了微小定义域限制的文本。而它自己对这种错误浑然不觉。

多智能体架构提供了一条绕过这个缺陷的路径：让多片概率云互相交叉验证。一个Agent走偏了，另一个可能发现漏洞；根Agent负责综合、检验、重试。这实际上是在工程层面模拟了人类数学家“提猜想→找反例→修正→再论证”的循环。

但光有这个还不够。

真正让这次发布站得住脚的，是Lean 4。这是一种形式化证明助手，可以把它理解成一个铁面无私的数学裁判。它有一个小而可信的验证内核，每一个证明步骤都必须严格对照数学公理被验证，结果只有两个：通过或失败。Astra生成的每一项论证都被转化成了Lean 4代码，编译通过意味着sorry count为零——没有任何未证明的步骤。

这就巧妙绕过了大模型的根本缺陷。Astra可以继续在概率云里天马行空，但最终产出的证明必须经过Lean 4的逐行刚性验证。形式化证书成了概率推理的外部地基校验器。

换句话说，这不是让大模型变严谨了，而是给不够严谨的大模型配了一个绝对严谨的数学裁判。

那Astra攻克的是什么级别的问题？随便列举几个：非sofic群的存在性构造（卡了27年）、推翻Connes刚性猜想（菲尔兹奖得主提出，悬了几十年）、球体堆积密度首次突破1978年的理论边界（48年）、多色Ramsey数超指数下界（解决Erdős第183号问题）。涵盖群论、算子代数、高维几何、极值组合学、计算复杂性、量子复杂性、格密码学、编码理论、离散几何——横跨多个领域。

这些都是人类顶尖数学家啃了几十年没啃下来的硬骨头。

当然，有些事实需要冷静看待。2000美元只是推理阶段的Token成本，不包括模型训练的天文数字投入，也不包括之前可能失败了多少次。Noam Brown也坦承Astra没能解决任何千禧年大奖难题，“尚未征服数学”。有数学家指出，虽然Lean验证了形式化证明正确，但形式化陈述是否准确对应了大家公认的开放问题，这一步仍然需要人类判断。

但这依然是一个分水岭。

在此之前，大模型在数学证明上被称为“强大的辅助”——能复现经典证明，能帮人展开论证步骤，能找到可能的反例，但无法自主攻克真正的开放难题。这个判断里隐含着一层意思：概率接龙机器不可能真正做数学。

现在这层天花板被撞开了一条大裂缝。

OpenAI明确声明所有数学论证都由AI系统生成，拒绝署名为人类。国际数学联盟刚刚背书了《莱顿宣言》，警告AI公司“绕过同行评审、威胁证明与署名的完整性”。OpenAI的回应很硬：Lean 4证书本身就是最强的信任凭证，不需要传统的同行评审来兜底。

这话说得冲，但确实有道理。传统同行评审依赖的是对审稿人权威的信任，而形式化验证让信任变成了一行行可执行的代码。你可以不信OpenAI，不信评审人，但你没法不信在自己电脑上跑出来的编译结果。

大模型本质上还是那个概率预测网络，它的“逻辑”还是模仿而非真正理解，它对矛盾还是没有本体论上的恐惧。但这些根本性缺陷没有被消灭，而是被工程手段绕了过去——直觉系统负责灵感和探索，符号逻辑系统负责严谨和兜底。两者被编排成一个完整的数学研究智能体。

这条路能走多远没人知道。但至少在这一天，一个会做数学的AI，不再是科幻小说里的情节了。