如果一家公司说自己的模型解了数学难题，最麻烦的问题往往很快出现：谁来确认它没漏掉一个条件，没把一个推导空格当成证明？8 月 1 日，OpenAI 给 Astra 的首次公开亮相选了一个硬场景。它没有走聊天产品发布路线，直接拿出 10 个数学与理论计算机科学结果，配套 249 页论文、GitHub 上的 Lean 形式化证书和每个解法的推理记录。
这次结果覆盖高维几何、编码理论、群论、算术电路复杂性、量子复杂性、格密码和极值组合等方向。OpenAI 的说法是，这些问题的主结果至少 10 年没有进展，多数更久；发现 10 个解所需 token 若按 Sol API 价格估算，约 2000 美元。这组数字很刺激，但更重的一点在验证方式：Astra 生成论证，人类和同一模型整理成稿，模型再把论证形式化成 Lean 证书。
这次先把证据摆出来
OpenAI 官方页面把 10 个结果列得很细。它包括高维球堆积新上界、任意最小距离下二进制码与球面码大小上界的指数级改进、非 sofic 群构造、Connes 刚性猜想反例、permanent 的算术公式下界、一般双人量子博弈的指数并行重复定理、欧氏最近向量问题的多项式因子近似困难性、Ehrhart 体积猜想、多色三角 Ramsey 数下界，以及 Erdős 两个极值图论问题。
官方论文摘要给出了可核的技术口径：比如 permanent 的公式下界是 n^4/log n 量级；最近向量问题通过从 3SAT 到 GapCVP 的确定性多项式时间归约得到 n^1/400 因子困难性；多色三角 Ramsey 数结果写成 R_k(3)=k^Theta(k)。这些并非产品营销里的性能分数，读者不能只看“十项突破”四个字，必须看对应问题、形式化文件和后续数学界复查。
GitHub 仓库也给了一个工程化入口。All.lean 汇总全部证明，单项文件包括 NonSoficGroup.lean、ConnesRigidity.lean、Permanent.lean、GapCVP.lean、QuantumParallelRepetition.lean 等；仓库声明使用 Lean 4.32.0、mathlib 和 Lake，构建命令是 lake exe cache get 后执行 lake build All。简单说，它交出的材料不止一篇 PDF，还把机器可检查的证明作为发布物的一部分。
2000 美元带来新压力
最容易被误读的数字是 2000 美元。它指 OpenAI 估算“找到这些解”所需 token 按 Sol API 价格折算的费用，不包括研究选题、提示设计、人工整理、形式化工程、外部复核和学术沟通。把这笔钱理解成“2000 美元买十个定理”，会把后面那些成本全抹掉。
但这个数字仍然有分量。数学发现过去常被描述成天才和多年直觉的产物，现在 OpenAI 把一部分搜索过程价格化：给出问题、让模型并行探索低概率路径、保留推理链，再让结果进入形式化检查。对研究机构来说，预算门槛可能下降；对数学共同体来说，审稿压力会上升，因为可提交的候选证明数量可能突然变多。
OpenAI 在责任声明里写道：
“claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.”
自然翻成中文，就是如果一份证明完全由 AI 生成，却署成人类独立完成，会同时歪曲系统贡献和人类智力劳动。这句话的分量不在姿态，在规则。Astra 这次把“AI 生成、人工整理、Lean 检查”拆开写清楚，等于给后续 AI 数学成果设了一套最低披露样板。
中文读者该看 Lean，而非只看榜单
国内讨论 AI 数学能力时，常被奥赛、FrontierMath、ARC-AGI 一类分数牵着走。分数有用，但它们仍是评测。Astra 这次把问题推进到另一层：模型产出的东西能否变成数学共同体愿意复查的对象，能否被形式化系统接住，能否在公开仓库里复现构建。
这对中国的模型团队和高校实验室有现实含义。第一，纯“我们模型数学很强”的说法会越来越弱，能否附带可检查证明、代码、数据和复现路径，会成为科研型模型发布的新门槛。第二，Lean 这类形式化系统会从小众工具进入 AI 研究基础设施，数学、计算机理论和安全证明都可能受影响。第三，AI 发现本身不等于学术共识，越是惊人的结果，越需要外部专家慢慢拆。
后续看三件事
这次发布仍有明显边界。Astra 是内部模型，外界无法独立复现实验搜索过程；OpenAI 负责正确性，但数学界还要审查论文中的概念选择、结果位置和已有文献关系；GitHub 证明能编译，也不自动等同于每个非形式化叙述都已完成学术确认。
所以后续可验证节点很具体：Lean 仓库能否被第三方顺利构建，相关领域专家是否接受这些结果的表述和归属，10 个证明里有没有因边界条件、定义选择或既有结果关系而被修订。若这三关走得稳，Astra 的意义才会超过一次公司发布会，变成 AI 参与数学研究的一个可引用先例。
OpenAI 把新模型家族第一次推到公众视野，没有选择客服、写代码或视频生成，选择了证明。这个选择本身就说明，前沿模型公司正在争夺的范围已超过用户时长，也包括“谁能产出可验证知识”的信誉。数学界会慢慢给答案，形式化工具会先给第一轮检查。
参考来源：OpenAI 官方研究发布、OpenAI 249 页证明论文、GitHub ten-proofs 仓库、CocoLoop、IT之家与 Developers Digest；核验 Astra 内部模型口径、10 个结果列表、Sol API 约 2000 美元 token 成本、Lean 4.32.0 构建方式、n^4/log n 与 n^1/400 等技术指标。