8月1日，OpenAI 公布了其未发布模型 Astra 的十项数学与理论计算机科学成果。按公司介绍，这批结果涉及多项长期开放问题，包括：非 sofic 群的存在性（自1999年悬而未决）、Connes 刚性猜想的反例（1980年提出）、高维球堆积密度上界的首次一般性改进（上一次是1978年）、量子并行重复的一般性证明、以及三个 Erdős 问题。每一份结果附带一个 Lean 4 形式化证明，任何人可以在本地编译验证。
OpenAI 称 Astra 生成全部十个解的总推理成本约为 2000 美元（按 Sol API 价格计算），论文、推理过程记录（walkthrough）和 Lean 证书均已在 GitHub 开源。公开这些材料，使外部研究者可以下载并尝试复现验证。
形式验证能回答的问题仍有范围限制。Lean 通过只意味着证明的逻辑步骤在形式系统内自洽，不等于形式化陈述完美对应了数学界关心的原始问题，也不等于新结果的意义、原创性和历史定位已经经过同行论证。数学界的独立评审刚刚开始。
十项结果涉及反例构造、密度上界和计算复杂度
这十项成果覆盖了六个学科分支，按问题的性质可以分为三类。
存在性与反例：非 sofic 群及 Connes 猜想。 最受关注的是非 sofic 群的显式构造。Sofic 群是 Mikhail Gromov 于 1999 年引入的概念，指那些可以通过有限置换系统任意逼近的群。所有 amenable 群和所有剩余有限群——数学家日常使用的几乎全部对象——都是 sofic 的。是否存在非 sofic 群，是现代群论最显眼的存在性问题之一。Astra 的构造表明答案是肯定的：至少存在一个群无法按 sofic 定义要求用有限置换系统逼近。对应的 Lean 证书已经通过编译，维基百科条目也已更新。
与 sofic 问题相邻的是 Connes 刚性猜想的反例。菲尔兹奖得主 Alain Connes 在 1980 年提出，具有 property (T) 的群是否总可以被其 von Neumann 代数唯一重构——简言之，这些代数结构是否"记住"了生成它们的群。Astra 构造了一族可数多个彼此不同构的群，却产生同一个 von Neumann 代数，否定了这个猜想及其有限到一的变体。
在极值图论中，Astra 给出了 Erdős-Simonovits 紧致性猜想的反例（经过修正的版本，针对圈图）和退化猜想的反例，分别对应 Erdős 问题 #180 和 #146。
上界改进：改进球堆积和编码理论中的一般界。 高维球堆积密度的最佳一般上界自 1978 年的 Kabatiansky-Levenshtein 界以来原地踏步。Astra 的结果并不给出更密集的排列方式，而是将 Cohn-Elkies 线性规划方法的极限精确确定了——其指数从约 0.599 提升至约 0.604。对应的编码理论结果同样严格改进了二元码和球面码的一般渐近上界。
下界与复杂度：永久式、最近向量问题及量子博弈。 Astra 证明了算术电路中计算永久式（permanent）的复杂度下界——这是近乎二次的电路下界和近乎四次的公式下界，虽非超多项式，但据手稿称是首个专门针对永久式的超线性下界。另一个结果将最近向量问题（CVP）的多项式因子近似硬度从之前的亚对数级推到了固定的 n^(1/400) 因子。在量子信息领域，Astra 给出了通用双玩家纠缠博弈的指数级并行重复定理，此前只有多项式衰减的一般结果。
另外两项成果涉及猜想证明与增长阶：Ehrhart 体积猜想被完整证明——对于重心在原点且唯一内格点为原点的凸体，最大体积的精确上界被确定；多色三角形 Ramsey 数的增长阶被确定为 k^(Θ(k))，回答了一个自 Erdős 原始提问以来关于根是否发散的问题。
OpenAI 数学研究负责人 Sébastien Bubeck 在 X 上称这些结果为"美丽的"，并指出这十个只是 Astra 已产出结果中的一部分样例。Noam Brown 补充了一个关键细节："我们没有在每个问题上花很多钱。测试时计算还可以推到更长。"但"令人遗憾的是，还没有千禧年大奖问题"。
Lean 可检查形式化证明，仍需核对原始数学问题
每一份 Astra 证明都附带一个存放在 GitHub 仓库 openai/ten-proofs 中的 Lean 4 证书。Lean 4 是一个基于依赖类型论的形式化证明助手，其用于校验的核心程序（trusted kernel）检查形式化证明是否符合规则。外部研究者可以安装相应工具链进行验证，但理解定理陈述与原问题的关系，仍需要数学知识。
独立分析机构 Kingy.ai 下载了该仓库（提交号 0fd01b1），在本地重建了工具链并执行 lake build All，在进程终止前至少完成了 9,007 个任务中的约 8,820 个编译。这不是一次完整的端到端构建，但它确认了工具链可复现、大部分项目可在本地编译。
但 Lean 验证与数学界接受之间有一个关键距离：Lean 只检查形式化编码后的论证，不检查形式化编码本身与原始数学问题之间是否存在偏差。具体来说，Lean 不能回答四个问题：
- 被形式化的定理陈述是否精确对应了数学界几十年来关心的那个问题？
- 所使用的定义和归约是否抓住了领域内的标准约定？
- 非形式化的上下文（哪些引理被省略、哪些边界条件被隐式处理）是否足以支撑"该问题已被解决"的结论？
- 结果的原创性和历史定位是否正确？
这些问题仍然需要数学家逐一审查。仓库本身也将这些证明标注为"agent-reviewed"（由 AI Agent 审查）而非人类独立审查。这是一个准确的定位：Lean 消除了大量局部逻辑错误的风险，但没有把定义翻译、文献判断和"这是否是我们想问的问题"变成机械事实。
专家已开始讨论，正式同行评审尚待完成
曼彻斯特大学数学家 Thomas Bloom——erdosproblems.com 的维护者——在 X 上称这批结果为"重大新闻"（big news），并表示其重要性超过了 OpenAI 5月发布的 Erdős 单位距离猜想反例。Bloom 的评价在此受到关注：2025年10月，正是他当场拆穿了 OpenAI 高管 Kevin Weil 宣称 GPT-5"解决了十个 Erdős 问题"的说法——实际是模型只是从文献中检索到了 Bloom 尚未收录的已有解。Weil 已于 2026 年 4 月离开 OpenAI。
认知科学家 Gary Marcus 在 X 上谨慎地指出，Astra 在特定数学形式上的能力并不意味着生成式 AI 的普遍可靠性问题——幻觉、规则遵循——得到了解决。"它甚至不意味着它能正确阅读 PDF，"Marcus 写道。
MathOverflow 上出现了一篇以"对数学研究公平性的严肃挑战"为题的讨论，作者是一位来自文理学院的数学家。该帖关注研究资源分配：作者指出，OpenAI 同时推出的"ChatGPT for Academic Researchers"计划——向符合条件的机构的 10 万名科学家和数学家免费提供前沿模型——正在制造新的资源不平等：不在指定机构名单中的研究者被排除在外。
多方报道指出，多位群论和算子代数专家（包括 Henry Bradford、Nathaniel Chapman、Ilya Dogon、Francesco Fournier-Facio）在论文中被致谢为提供过咨询，但致谢不等同于公开背书。整体而言，数学界目前的状态是：论文与形式化材料已经公开，但没有任何一项成果已经完成正式的同行评审流程。
Astra 采用多 Agent 协作，面向持续较久的研究任务
OpenAI 将 Astra 描述为"下一个主要模型家族"（next major model family），与当前的 Sol、Terra、Luna 系列并列。其架构特征是多 Agent：一个根 Agent 创建子 Agent，分发问题片段，等待结果，合成最终答案——专门为持续数小时甚至数天的长程任务设计。
这一架构最早出现在5月 Erdős 单位距离猜想的反例中（Fields 奖得主 Tim Gowers 当时表示会"毫不犹豫地推荐发表"），7月的评估安全事件也引发了对长任务模型的关注，但不能仅凭这类报道，把所有涉事模型都认定为 Astra。8月的十项数学成果展示了其研究用途。
Sam Altman 于 7 月 29 日在华盛顿特区向参议员 Raphael Warnock 和 Bernie Moreno、财政部长 Scott Bessent、商务部长 Howard Lutnick 等官员闭门演示了 Astra。该模型预计将成为首批接受 EO 14409 框架下联邦预发布评估的系统之一。
关于 Astra 是否会以 GPT-6 名义发布，目前没有确认。Astra 可能作为 GPT-5 系列的一个点版本（如 GPT-5.7），也可能成为独立模型家族。OpenAI 首席科学家 Jakub Pachocki 此前曾描述公司目标是 2026 年 9 月拥有"研究实习生级别"的 AI 科学家能力，2028 年初实现"完全自主 AI 研究员"。十项 Lean 验证的成果是这条路线上的中期证据，而非终点。
低推理费用之外，选题、验证和理解仍需人力
如果这十项成果中的大多数通过了同行评审，它们将为评估 AI 研究的成本和验证方式提供重要案例。
首先，攻克的边际成本。按 OpenAI 的口径，这批十项结果的总推理开销约为 2000 美元，并非每个问题的费用，也不包含模型训练、人工整理和验证的全部成本。Noam Brown 表示还可投入更长的测试时计算，这并不等于费用必然继续下降。如果类似结果能够复现，研究资源的分配也可能变化：从前，问"谁能解"是核心瓶颈；未来，"谁能问对问题、谁能在 AI 产出的候选结果中识别重要发现、谁能把结果编织成有意义的理论"可能成为新的稀缺能力。
其次，形式化验证材料的公开。Lean 4 正在成为 AI 数学领域的通用验证后端——DeepMind 的 AlphaProof Nexus 和 OpenAI 的 Astra 都选择了同一套基础设施，其社区数学库 mathlib 包含超过 21 万个形式化定理。这意味着结果的跨实验室可比较性正在建立，不需要信任任何单一方的声明。
但这种转变也带来了新的不平等。如果 OpenAI 的前沿模型只向特定机构的研究者免费开放，而 Astra 本身不公开发布，那么能够参与"AI 辅助数学发现"的研究者将被限制在有访问权限的群体内。MathOverflow 上的担忧正是这个问题的早期信号。
最后，理解的速度。十个结果同时发布，跨越六个学科分支，会同时占用多个领域专家的审查精力。验证可以通过 Lean 自动化，但理解——将结果置于理论脉络中、提取可推广的方法、重新校准相关领域的研究方向——仍然是一个以年为单位的慢过程。数据科学家 Josef Waples 在 DataCamp 的分析中指出，证明一个定理与理解一个定理确实是两件不同的事。在这十个结果的案例中，产生候选证明与完成理解之间的时间差更值得关注。
后续看专家逐项审查，不能以编译进度代替结论
独立专家对每个结果的逐项审计是最紧迫的下一步。对于非 sofic 群和 Connes 刚性这样的核心猜想，审计将集中于形式化陈述是否精确覆盖了领域内公认的问题表述。对于球堆积和编码理论的上界改进，重点在于层次结构是否确实"严格"改进了所有已知界。Kingy.ai 已将十项成果列入其数学与科学突破追踪器的 Tier 1（暂定）：主要证据公开、Lean 形式化可用、AI 参与直接、独立专家评审待完成。
OpenAI 已经交付了可供审查的原材料——论文、推理记录、可编译的 Lean 证书。从"可检验"走到"被检验完毕"，还需要逐项复核和必要的修订。
（声明：OpenAI 在发布中明确表示数学论证由 Astra 生成，人类研究者协助整理手稿和形式化证明，OpenAI 对方案的正确性承担责任。该声明引用了国际数学联盟背书的《莱顿宣言》，该宣言要求人和机构对 AI 辅助的数学主张保持责任归属。）
