2000 美元破解十道数学难题！OpenAI 亮相 48 小时后，一个人站出来说：这是虚张声势

luyuanhong

2000 美元破解十道数学难题！OpenAI 亮相 48 小时后，一个人站出来说：这是虚张声势

原创  BaselineModel  零号模型  2026 年 8 月 4 日 17:48  北京

8 月 1 日，OpenAI 丢出一颗核弹。

这场震动来自一篇数学博客，与产品发布会、API 降价或完整的模型技术报告都无关。

标题平平无奇：《数学与理论计算机科学的十项进展》。

内容却让全球数学界集体失语：他们的下一代模型 Astra ，一口气在十个“至少十年没有核心进展”的开放问题上取得了新结果。

高维球堆积、非 sofic 群的存在性构造、Connes 刚性猜想的反例、算术电路复杂性新下界、多色 Ramsey 数的超指数下界……随便拎出一个，都是能让一位数学家用整个职业生涯去啃的硬骨头。

而 Astra 解决这十道题的全部推理成本，按照 Sol 系列 API 的公开价格折算，

不到两千美元。



▲ OpenAI 研究者 Noam Brown 在 X 上宣布这一成果，互动量爆表

一篇博客里“夹带”了一个新模型

先说一个被很多人忽略的细节

Astra 这个名字，是在这篇数学博客的第三段里悄悄出现的。

OpenAI 省去了独立发布会、Sam Altman 站台和倒计时海报。

科技媒体 Gizmodo 把这种安排概括为：“OpenAI 把下一代模型的发布，夹带进了一篇数学博客里。”

此前 The Information 等媒体称，这个模型面向长时间运行任务，可协调多个agent，处理复杂项目与高等数学。

OpenAI 已有 Sol 、Terra 、Luna 等命名序列，Astra（拉丁语"星"）显然是下一代主力。

但 OpenAI 选择了一种极其聪明的亮相方式：不告诉你它是什么，先让你看它能做什么。

做了什么呢？

249 页的数学手稿 PDF ，公开仓库 openai/ten-proofs 中的完整代码，以及，关键中的关键，Lean 形式化证书。


▲ 公开的 Lean 证明仓库，任何人都可以机器验证

这里需要做一个小科普

Lean 是一种交互式定理证明器：你写出形式化的证明步骤，机器内核会逐步检查每一步是否合法。

它不能帮你“发现”证明的直觉，却能把“看起来对”变成“机器说它对”。

Astra 的部分结果因此成为可以被任何人独立运行验证的数字制品，可信度不只依赖 OpenAI 的博客。

这也正是数学领域如此特殊的原因，它是少数可以被完全形式化判定对错的人类知识领域。

两千美元的成本盲区


▲ Brown 强调：十项突破的证明生成合计不到 2000 美元

OpenAI 研究者 Noam Brown 在宣布之后迅速补了一条推文：生成这十个证明的成本合计不到两千美元。

潜台词呼之欲出：你看，科学发现的边际成本正在趋近于零。

但 Brown 自己也承认了另一面：


▲ Brown 坦言：试过其他重大问题未果，千禧年大奖问题尚未攻克

试过其他重大问题，失败了。千禧年大奖问题？没戏

而且“每道题其实没投入太多算力，还可以继续加压”。

这里有一个被巧妙模糊的会计问题。

两千美元是边际推理成本，也就是 Astra 这个已经训练好的模型，在跑这十道题时消耗的 token 费用。

它不包含训练 Astra 本身的天文数字沉没成本，也不包含那些花了钱却没解出来的题的费用。

正如独立博主 Simon Willison 尖锐地追问：“我想看到所用的提示词。

以及，花了两千美元却没解出来的题，到底有多少？”

然后，Gary Marcus 来了

如果你关注 AI 圈的论战，你一定认识 Gary Marcus 。

这位纽约大学的认知科学家、连续创业者，大概是英语世界里对生成式 AI 最持久、最系统、最不留情面的怀疑论者。

在 Astra 数学结果公布的同一天，Marcus 发出了他的第一轮“热评”：印象深刻，但，



▲ Marcus 承认结果令人印象深刻，但强调数学领域的特殊性

他的核心论点，在第二天的长文《关于 Astra 数学结果的八大误解》中被压缩成了一个简洁的逻辑链：

数学是特例

它有形式化的真值判定标准，可以用程序自动生成海量带标签的训练数据，可以用 Lean 这样的验证器过滤幻觉。

编码有类似性质。

但绝大多数现实世界的任务，例如从任意 PDF 中可靠抽取数字、为特定创作者写视频脚本，都缺少这种结构。



▲ Marcus 系统性地列出了公众对 Astra 结果的八个认知偏差

他举了一个经典的历史类比：IBM Watson 在 2011 年赢下 Jeopardy 问答节目，震惊世界。

然后 IBM 试图把它卖到癌症诊疗领域。

结果呢？

公开的、昂贵的、持续数年的失败和战略收缩。

一个封闭域的演示震撼，并不能自动迁移到充满噪声、责任和分布外案例的开放世界。

有人拿 Anthropic 的模型 Fable 去评价 Astra 的结果，得出了“今天或许是数学史上最重要的一天”这样的惊叹。

Marcus 立刻回击，


▲ Marcus：把 Astra 首日与微积分、代数、零的概念并列？荒谬。

即便这些结果达到了菲尔兹奖的水平，也不等于数学被“解决”了。据我理解，这次并没有发展出新的理论或新的技术。数学的许多角落可能仍是 Astra 不擅长的。

更尖锐的质疑：经济账

8 月 3 日，Marcus 把技术质疑和经济质疑焊在了一起，争论随之变得更加尖锐。

他引用了投资者 Ross Hendricks 的一段分析：

Hendricks 认为，超大规模云厂商据以支撑巨额资本开支的 AI 收入，很大程度上可以追溯到 OpenAI 和 Anthropic 的算力需求。

一旦这两家的市场份额被低成本替代方案侵蚀，相关基础设施投资可能承压。

这是一种市场情景推演，缺少经审计数据支持。

随后 Marcus 给出了自己的判断，


▲ 种子推文：Astra 没有对照组，也许并不比 Fable 好多少，绝非 ASI ，或许是在转移对糟糕经济账的注意力

他认为 Astra 缺少对照组，相比 Fable 的优势仍未得到证明，离 ASI 也很遥远；

这场发布或许意在转移外界对经济状况的关注。

Marcus 称 OpenAI 在虚张声势，而自己拆穿了这套说法。

这属于动机推断，审计结论和财报分析都无法为其背书。

但它叠加在了一个已经存在数月的产业焦虑之上，因此击中了不少人的神经。

独立科技评论人 Ed Zitron 在 6 月底就发表了万字长文《AI 行业正在输》，从国际清算银行年报切入：五大 hyperscaler 在 2025-2026 年 AI 相关资本开支可能超过万亿美元量级，开支增速远超盈利和自由现金流。

有分析师估算，整个行业需要约 6500 亿美元的新增年收入，才能让这些基础设施投资获得 10% 的合理回报。

而当前可归因于 AI 的收入，即便按最宽口径计算，也远低于此。

当资本开支预期依靠“能力神话”来供氧时，任何一次高可见度的技术突破，都会同时面对科学与金融尺度的检验：前者问“证明成立吗”；

后者问“能改善单位经济吗”。

反批评的反批评

Marcus 当然也挨了不少批评


▲ 回复区的质疑：你是否在指控 OpenAI 的研究者全体撒谎？

有人追问：Marcus 是否在指控 OpenAI 研究者集体为雇主撒谎？

如果 Astra 最终被证明远强于 Fable ，他会不会再度改口？

对方由此指责他不断移动球门柱

还有人讽刺："以前你说 AI 连基础数学都不会，现在它解了十年级难题，你又说数学本来就简单。"

但也有人提出了更有建设性的反驳角度，

即便 OpenAI 和 Anthropic 流失客户，云厂商仍可托管其他模型来销售算力。

Hyperscale r的收入结构可能重组，归零并非必然结果。

Marcus 把“前沿实验室的经济困境”等同于“整条供应链崩塌”，在逻辑上跳了一步。

尾声：证明与账本

Astra 的 Lean 证书、公开仓库和十项结果，都值得数学共同体继续检验。

两千美元这个数字也有明确边界：它只覆盖公司口径下的证明生成成本，训练投入、失败尝试和人工整理仍在账外。

Marcus 把一次数学发布解释成经济压力下的注意力转移，目前只能算带有立场的猜测。

技术成果能否经受独立复核，商业价值能否覆盖庞大投入，终究要由证明和账本分别回答。

零号模型