8月2日凌晨，OpenAI 悄悄挂出一篇 249 页的论文。

不是产品发布会，不是模型更新日志，是 10 项数学和理论计算机科学难题的证明，每项都附 Lean 4 形式化验证证书。

模型名字第一次公开，叫 Astra。拉丁语「星群」。

十道题里，最短的开放了 10 年，最长的困扰学界超过半个世纪。高维球体堆积密度上界，48 年来第一次推进。三项成果直接推翻长期猜想，两项解决厄尔多什悬赏问题。

OpenAI 按当前 GPT-5.6 Sol 的 API 费率算了一笔账，模型找到全部 10 个解法消耗的 Token 成本，大约 2000 美元。人类只是整理论文和做 Lean 验证，数学论证由 AI 生成。

这不是「人类写的，是人类检查的」。

Sam Altman 本周在华盛顿向白宫官员、内阁成员和国会议员预览了 Astra。政策制定者比公众早一天知道。10 项数学突破本身就是一种政治信号。

AI 不只是工具，开始能啃硬骨头了。名字起得挺好，星群，不是恒星。

OpenAI Astra AI数学 Lean4验证