OpenAI 把 Astra 亮出来了
OpenAI 把 Astra 亮出来了
8 月 2 日凌晨，OpenAI 悄悄挂出一篇 249 页的论文。
不是产品发布会，不是模型更新日志，是 10 项数学和理论计算机科学难题的证明，每项都附 Lean 4 形式化验证证书。
模型名字第一次公开，叫 Astra。拉丁语「星群」。
这十道题，开放时间最短的也有 10 年，最长的困扰学界超过半个世纪。
OpenAI 说，解法的成本大约 2000 美元。
球体堆积，48 年来第一次推进
1978 年，Cohn–Elkies 给出了高维球体堆积密度的一个上界阈值。
48 年过去，没人能把它往前推一寸。
Astra 给出了新的上界，把结果推进到 Cohn–Elkies 阈值本身。这不是「找到一个更优的解」，是把一堵墙的厚度削薄了一点，让后面的人能继续往前挖。
论文里说，这是「一般球体堆积指数自 1978 年以来的首次改进」。
一行进步，半个世纪的等待。
推翻三个长期猜想，不是打补丁
三项成果，不是「优化」，是直接「推翻」。
非 sofic 群。2000 年前后，群论里有个核心猜想，所有可数群都是 sofic 群。Astra 构造出了一个明确的反例，直接把这个猜想推翻。
Connes 刚性猜想。长期认为某些群可以由其对应的冯·诺依曼代数唯一确定。Astra 证明，不同的群也能对应同一个冯·诺依曼代数。
Ehrhart 体积猜想。确定内部只有一个格点、且该格点恰好在重心的凸体，在任意维度下能取到的最大体积。
这不是在既有结论上打补丁，是告诉学界，「你们之前默认的方向，有些是错的」。
算术电路、量子博弈、格密码，全在场
十项成果里，有三项跟计算复杂性直接相关。
算术电路复杂性。用算术电路和公式计算积和式，给出新的下界，公式下界达到 n⁴/log n 量级。
量子并行重复。证明适用于一般双人量子博弈的指数级并行重复定理，把经典复杂性理论的基础原理扩展到了量子博弈场景。
最近向量问题。证明最近向量问题具有多项式因子的近似困难性。这个问题是格理论的基础问题，与后量子密码学直接相关。
换句话说，Astra 不只是会算数，它在啃那些「算不出」的边界。
多色拉姆齐数，厄尔多什的第 183 号问题
保罗·厄尔多什是 20 世纪最传奇的数学家之一，他生前留下过一串「悬赏问题」。
Astra 这次解决了两个。
多色拉姆齐数。给出多色三角形拉姆齐数的超指数下界，这是厄尔多什第 183 号问题。
极值数猜想。在极值图论的紧致性猜想和退化性猜想上的结果，对应厄尔多什第 146 号和第 180 号问题。
厄尔多什当年用「奖金」悬赏这些问题，有的几美元，有的几千美元。他大概没想过，最后来领奖的会是一个 AI。
成本 2000 美元，人类只是整理
OpenAI 按照当前 GPT-5.6 Sol 的 API 费率算了一笔账。
模型找到全部 10 个解法，消耗的 Token 总成本，大约 2000 美元。
随后，人类研究人员借助同一模型，把论证整理成论文，再由模型把每项论证转化为 Lean 形式化证明证书。
OpenAI 的表述很克制，「公司参与了论文整理和 Lean 形式化验证，并对结果的正确性负责，但其中的数学论证由 AI 系统生成」。
不是人类写的，是人类检查的。
为什么用 Lean 4，而不是「相信我」
数学证明最怕一句话，「相信我，这一步显然成立」。
Lean 4 是形式化证明语言，每一步推理都要被机器检查。你不能跳步，不能模糊，不能「显然」。
Astra 给出的 10 项成果，每项都有 Lean 证书。GitHub 仓库已经公开，任何人都可以跑一遍验证脚本。
这不是「我们觉得是对的」，是「你可以自己检查它是对的」。
这也是为什么 OpenAI 敢在论文署名问题上表态。如果证明完全由 AI 生成，却署名人类作者，会同时歪曲 AI 的贡献和人类原创工作的性质。
所以论文作者写的是 OpenAI，不是哪个人。
政策圈已经看过，公众今天才看见
The Information 昨天报道，Sam Altman 本周在华盛顿向白宫官员、内阁成员和国会议员预览了 Astra。
政策制定者比公众早一天知道。
这不是巧合。10 项数学突破，三项推翻长期猜想，两项解决厄尔多什悬赏问题，这种成绩单本身就是一种政治信号。
AI 不只是工具，开始能啃硬骨头了。
三个信号，一个悬念
信号一，AI 系统参与数学研究的模式已经清晰。从「人类提问、AI 辅助计算」，变成「AI 找解法、人类检查论证」。
信号二，OpenAI 开始展示下一代模型在科研场景的能力。不是跑分，是直接上论文。
信号三，形式化验证正在成为「AI 证明」的标准配置。Lean 证书的存在，让争议空间变小，也让「对不对」这件事可以被机器裁决。
悬念是，Astra 能不能把这种能力稳定扩展到物理、生物、工程等领域。
数学是另一个世界，规则清晰、边界封闭。真实世界的问题，往往没有唯一的正确答案。
但至少在 8 月 2 日这一天，OpenAI 用 249 页论文和 10 个 Lean 证书，告诉所有人，Astra 不是下一个聊天模型，是下一个能自己啃题目的模型。
名字起得挺好。星群，不是恒星。