Astra 花 2000 美元证出 10 道数学难题，这件事让我重新看 AI 的边界

8 月 2 日早上，我刷到 Greg Brockman 的一条推文。内容很短，但数字很刺眼，OpenAI 内部代号为 Astra 的下一代模型，用大约 2000 美元的成本，证出了数学与理论计算机科学领域的 10 项重大进展。

这些结果包括非 sofic 群的存在、Connes 刚性猜想的反例、von Neumann 代数、高维球堆积、电路复杂度。OpenAI 把全部证明、Lean 证书和 CoT 逐步推导过程都公开了。按 Sol API 的价格折算，一个结果平均不到 200 美元。

我的第一反应不是「AI 要拿菲尔兹奖了」，而是「一个博士后一个月的人力成本，模型几个小时就花完了」。这种反差太大了，大到让人先愣住，再开始怀疑。

这件事到底说了什么

先回到事实本身。根据 Brockman 的披露，这次用的是 Astra 的内部版本，不是公开 API 上那个面向消费者的 ChatGPT。Astra 通过 Sol API 完成推理，总调用成本约 2000 美元。

它产出的不是代码片段，也不是文献综述，而是形式化的数学证明。每一个结果都附带 Lean 证书，你可以把证明放进 Lean 证明助手里去跑。这很重要，因为这说明形式化验证这一关，它自己过了。CoT 逐步推导也被公开，方便别人检查它是怎么想出来的。

我把公开列表反复看了几遍。非 sofic 群的存在是一个长期悬而未决的问题。Connes 刚性猜想的反例如果成立，算子代数领域会有一大批教科书需要重写。von Neumann 代数、高维球堆积、电路复杂度，这几个方向每一个都够一个研究团队做几年。

不是说 AI 把这些领域一锅端了，而是它能在一次实验里同时覆盖这么多不同方向，还给出形式化证明，这件事本身就是新信号。

为什么这和以往的 AI 数学故事不一样

过去几年，AI 做数学的路径通常分两类。一类是专用系统，比如 Google 的 AlphaGeometry，它只解决几何题，靠符号搜索和强化学习在特定领域里面横着走。另一类是辅助猜想，LLM 负责提出假设、生成模式，然后人类数学家去证。

Astra 这次不太一样。它不是几何专用模型，也不是只负责猜想的副驾驶。它更像一个通用推理引擎，把问题形式化、搜索证明、验证结果这条链路自己跑通了。而且它的成本不是百万美元，是几千美元。

这个差别很关键。专用系统做到顶尖，只能证明「AI 在狭窄领域很猛」。通用模型做到这一步，说明「推理能力本身在规模化」。更直白地说，Astra 不是被训练成数学家，而是被训练成会思考的通用模型，结果数学成了它能力溢出最明显的场景之一。

我以前觉得，大模型在数学上最实用的位置是帮助人类整理思路、验证步骤。现在看来，这个定位可能太低了。它们开始具备独立完成中等难度研究探索的能力。注意我说的是中等难度，不是顶级难题。顶级难题需要的不仅是推理，还有对问题结构的深层直觉，这一点 AI 目前还不稳定。

skepticism 必须有，而且要放在前面

写到这里，我必须停下来泼一盆冷水。Formal proof 只能证明形式化后的命题是对的。如果形式化过程本身有偏差，那 Lean 证书再漂亮，证的也是一个错误的问题。

这不是假设。今年 7 月，GPT-5.6 Sol 对循环双覆盖猜想给出过证明，社区的反应就很谨慎。不是质疑模型能力，而是质疑形式化陈述和原问题是否完全一致。历史上，数学里这种「看起来证了，后来发现条件被偷偷改弱」的例子太多了。

Astra 这次更难判断。Connes 刚性猜想的反例如果成立，影响太大，大到业界必须反复核验。非 sofic 群的存在也是。任何一个方向的证明都需要领域专家逐行看，看模型有没有把某个假设默认当成已知，有没有把不等价的命题当成等价。

还有一个容易被忽略的点。CoT 公开是好事，但 CoT 本身也可能有说服性错误。模型在推理链里写得很顺，不代表每一步都严格。Lean 证书只能检查最终形式化步骤，CoT 里那些从自然语言到形式化的跳跃，依然需要人来审计。

所以我现在的态度是，震撼归震撼，但先别急着宣布数学革命。等六个月，看看有没有数学家确认这些结果，再下结论也不迟。

对工程平台来说，这该怎么理解

把数学讨论放一边，这件事对我这种做 AI 工程的人，冲击其实更直接。

我们在平台上做的事情，是把模型封装成服务、给 Agent 搭工具链、做预算和限流。以前我们做这些，主要是服务聊天、写代码、总结文档。Astra 这件事告诉我们，下一代模型的主要任务，可能是做推理和验证，而不是单纯生成文本。

这对平台架构的影响是实实在在的。第一，Agent 的工具箱里需要加入形式化验证器，比如 Lean、Isabelle、Coq。模型产出的不只是字符串，而是可以被外部系统判对错的结构化对象。第二，推理成本模型要重新算。按 Sol API 的价格，2000 美元能跑 10 个研究级探索，那企业内部的知识库、代码重构、系统审计，成本结构会完全变样。第三，人机协作的界面要升级。以前是一个人让模型写一段代码，自己 review。以后要变成模型给出一个证明或方案，人和外部验证器一起检查。

我在做 LangGraph 相关的工作，感触特别深。LangGraph 的核心价值是把 Agent 的循环状态管理清楚。未来一个 Agent 的工作流，很可能是「提出假设 -> 形式化 -> 调用证明器 -> 反馈修正 -> 输出报告」。这个循环里的每一步都需要状态、分支、人工门控。如果 Astra 代表的趋势是真的，那 LangGraph 这种框架会变得越来越重要，因为它能帮我们把这种复杂推理链的每一步都管起来。

对人类研究者的角色，该怎么重新理解

很多人一看到这种新闻，本能反应是「数学家要失业了」。我的判断相反，数学家会变得更值钱，但不是以他们现在的工作方式。

AI 擅长的是把已知形式化后的搜索空间炸开。它不擅长的是提出好问题。什么叫好问题？就是既重要又可证、形式化后不会失真、证明结果能带来新结构的问题。这恰恰是人类数学家的核心能力。

未来的分工可能是这样。人类负责把模糊的科学直觉变成精确的问题，定义清楚假设和边界。AI 负责在这个边界里快速尝试、验证、失败、再尝试。人类再负责检查结果是否真正回答了原问题，并把它嵌入到更大的理论图景里。

这种结构下，AI 不是替代者，而是放大器。它放大的是人类的探索半径。一个数学家一辈子能做几个大问题？如果 AI 把探索成本压到几小时一次，一个研究团队可以尝试的方向数量会指数级增长。但这也意味着学术评价体系要变，同行评审要变，发表机制也要变。否则会出现「证明洪水」，里面夹杂着大量形式上正确但意义不大的结果。