八月一日，OpenAI 把一张不太像产品发布的清单钉上了研究页：内部版 Astra 在高维几何、编码理论、群论、算数电路复杂度、量子复杂度、格密码相关问题与极值组合里，一口气交出十项「解决或大幅推进长期公开问题」的结果。官方写得很具体——找这些解法所耗的 token，按 Sol API 价大约只要两千美元；随后由人与同一模型把论证整理成手稿，再由模型把每条论证形式化进 Lean 证书，并公开模型「怎么想」的叙述录音式文本。
这不是「模型会刷题」的软软新闻。清单里能听见具体钉子声：任意给定最小距离下二元码最大规模的指数级改进，以及高维球面码的对应结果；构造出非 sofic 群，顶上群论里的老问题；否证「某些群由其 von Neumann 代数唯一决定」的猜想；永久式（permanent）的算数公式下界到 n⁴/log n 量级；一般两方量子博弈的指数级并行重复定理；与后量子密码相关的最近向量问题近似硬度；在每一维确定「质心是唯一内部格点」的凸体最大体积（Ehrhart 体积猜想相关）；多色三角形 Ramsey 数的超指数下界（Erdős 问题 183）；以及极值图论里紧性与退化猜想的进展（Erdős 问题 146、180）。更早一点，他们还在评测未发布模型时，放出过对 Erdős 单位距离猜想的反证，并说那条线已带动后续工作。
钱和证书把故事钉死了。两千美元不是「便宜得可笑」的噱头，而是把前沿数学探索写成可计价的推理预算：贵的不再是一张纸上的灵感，而是能不能把搜索、写稿、形式化串成一条可复查的流水线。Lean 证书与思考叙述一起放出，等于把「模型想出了什么」和「机器验证了什么」拆成两层——前者仍可能有争议，后者至少能被数学共同体按证书打开。OpenAI 自己也划清署名：若证明基本由 AI 生成，却署成纯人类作者，会同时歪曲系统贡献与人类智力劳动；他们参与手稿整理与形式化，并对正确性负责，但论证本身来自系统。这是对 Leiden「AI 与数学」宣言一类担忧的正面回应，不是公关口号。
行业含义比「又刷了一份榜」硬。第一，研究评测开始从封闭基准挪到开放问题本身——模型在开发期就被丢进仍未解决的题，成功案例会反哺训练叙事与产品叙事（Astra 本来就要当「下一代主力」讲）。第二，形式化成了交付格式：没有 Lean，这类声明很难跨过「你们是不是自嗨」的门槛；有了证书，竞争维度变成「谁能稳定产出可检证明」。第三，署名与优先权会更吵——期刊、会议、博士生培养若继续假装作者栏只有人类，会被这批结果直接打脸；反过来，若把模型写成共同作者却不交代流水线，也会把优先权搅浑。
争议同样具体。两千美元的搜索成本，不等于社区复现成本：内部 Astra、数据污染风险、提示与工具链、算力配额，都可能把「公开的十道题」变成「只有实验室能复跑的十道题」。形式化验证正确，也不自动等于证明「有数学品味」或「会提出好问题」——目前官方展示的是推进与解决，不是让模型自己定义下一个 Erdős 列表。把 10 万科学家的免费 ChatGPT 名额（Academic Researchers 计划）与这批结果并排放，更像在铺入口：一边发证明，一边发账号，数学共同体被同时拉进工具与署名政治。
我的判断很直白：这篇文章真正值钱的，不是十个标题里的形容词，而是「搜索预算 → 手稿 → Lean → 公开叙述」被写成可审计的科研交付物。若后续系统卡与独立复核站得住，数学研究的瓶颈会从「有没有人能想到」部分转向「有没有人能审、能教、能把机器证明嵌进人类理论图景」。审稿人与导师的工作不会消失，只会更像质检与意义分配。读者若只记住「AI 证明了十道题」，就漏掉了 OpenAI 真正想推广的那条流水线。