先说结论：OpenAI 确实首次公开提到了 Astra，并称其为“我们的下一代主要模型（our next major model）”，但这不是一次面向用户的模型发布。 截至 2026 年 8 月 5 日，OpenAI 没有宣布 Astra 的发布日期、API 型号、价格、ChatGPT 开放范围，也没有确认它最终会叫 GPT-6。普通用户现在无法在 ChatGPT、Codex 或 API 中选择 Astra。
这次官宣的核心是研究成果：Astra 的一个内部版本在数学和理论计算机科学中给出了 10 项新结果。它们有的解决了长期开放问题，有的显著推进了已知边界；OpenAI 还公开了对应的 Lean 4 形式化证明代码。
Astra 尚未开放。想先使用当前可用的 ChatGPT 与 Codex 模型，可查看 Plus / Pro 套餐；Astra 开放后，本文会继续更新入口、权限和使用方式。
OpenAI 这次真正官宣了什么
2026 年 8 月 1 日，OpenAI 发布了《Ten advances in mathematics and theoretical computer science》。官方原文的关键表述是：“an internal version of Astra, our next major model”，即“我们的下一代主要模型 Astra 的一个内部版本”。
这句话能确认两件事：
- Astra 是 OpenAI 正在研发的下一代主要模型相关名称，而不只是外界传闻。
- 产生这批结果的是内部版本，不是已经在 ChatGPT 或 API 上线的公开产品。
它不能确认 Astra 是最终商品名，更不能直接推出“Astra 就是 GPT-6”。官方公告没有模型卡、系统卡、API model ID、开放套餐、价格或发布日期，因此更准确的定性是：这是下一代模型的研究能力展示，不是产品发布会。
需要特别注意，OpenAI 的公告标题用的是“ten advances（十项进展）”，不是“ten problems solved（解决十道难题）”。把全部十项都写成“彻底攻克十道未解题”会夸大官方结论。
Astra 完成的 10 项结果是什么
OpenAI 在 ten-proofs 开源仓库 中列出了十项结果及对应 Lean 文件。下面用非专业读者也能理解的方式概括其意义：
| # | 方向 | 这次取得的结果 |
|---|
| 1 | 高维球堆积 | 改进高维空间中球体最密堆积问题的渐进上界，达到 Cohn-Elkies 阈值。这是边界推进，不是解出所有维度的球堆积问题。 |
| 2 | 二进制码与球面码 | 对每一种最小距离给出指数级更强的二进制码上界，并得到相应的球面码结果。 |
| 3 | non-sofic 群 | 构造出一个 non-sofic 群，否定“每个群都能被有限置换近似”的可能性。该问题通常追溯到 1999 年，因此常被概括为约 27 年未解。 |
| 4 | Connes 刚性猜想 | 给出反例，说明某些群不能仅由其群冯诺依曼代数唯一确定。 |
| 5 | 算术电路复杂度 | 提升计算 permanent（积和式）的算术电路与公式下界，其中包含 n^4 / log n 的公式下界。 |
| 6 | 量子并行重复 | 对任意有限双人量子游戏证明指数级并行重复结论。 |
| 7 | 最近向量问题 | 推进 CVP 的多项式因子近似困难性，并给出与译码、格问题相关的推论。 |
| 8 | Ehrhart 体积猜想 | 给出所有维度下的尖锐最大体积：研究对象是重心为唯一内部格点的凸体。 |
| 9 | 多色 Ramsey 数 | 给出多色三角 Ramsey 数的超指数下界，并解决 Erdős 问题 183。 |
| 10 | 极值图论 | 为紧致性猜想和退化性猜想构造反例，并解决 Erdős 问题 146 与 180。 |
这组结果覆盖几何、编码理论、群论、算术电路、量子复杂性、格问题和极值组合等多个专业方向。真正值得关注的不是“模型会做竞赛题”，而是它尝试完成了提出新构造、寻找反例、改进理论上下界，再把论证转成机器可检查证明的完整研究流程。
“成本约 2000 美元”到底是什么意思
网上常见的“Astra 花 2000 美元解决十道难题”并不准确。OpenAI 的口径是：把这项研究消耗的模型 token 按 Sol API 费率折算，约为 2000 美元。
这不是 Astra 的售价，也不是训练 Astra 的成本，更不是整个研究项目的总预算。它不包含模型训练、研究人员时间、基础设施、形式化工程和学术验证等成本。更稳妥的理解是：如果只核算本项目中的推理 token，并用当前 Sol API 价格估值，量级约为 2000 美元。
所以，不能据此推断未来 Astra API 会很便宜，也不能推断普通用户花 2000 美元就能复现全部结果。
Lean 4 全形式化验证意味着什么
OpenAI 为十项结果分别公开了 Lean 4 文件，并提供统一构建入口。Lean 会检查形式化证明能否从声明的定义、公理和已验证依赖中逐步推出结论；这比只发布自然语言推导更容易发现漏步或逻辑跳跃，也便于其他研究者复现。
但“Lean 通过”不等于所有争议都已经结束。外部研究者仍需检查：自然语言命题是否被准确翻译成形式化陈述、采用的前提是否符合原问题、结论是否真正新颖，以及它在所属领域的重要性。机器验证强化了正确性证据，但不能替代独立复核和同行评审。
有 Lean 环境的读者可以直接查看 openai/ten-proofs。仓库目前使用 Lean 4.32.0、mathlib 和 Lake，并给出了完整构建命令。
Astra 会是 GPT-6 吗
目前唯一可靠答案是：不知道。
OpenAI 只把 Astra 称为“下一代主要模型”，没有写“GPT-6”，也没有说明 Astra 是内部代号、模型家族名，还是最终面向市场的名字。模型在研发期与发布时采用不同名称并不罕见，因此下面两种说法都超出了现有证据：
- “OpenAI 已正式把 GPT-6 命名为 Astra”；
- “Astra 一定不会叫 GPT-6”。
在 OpenAI 公布正式产品页、模型卡或 API 文档前，标题中可以讨论“Astra 是否是 GPT-6”，正文则应保留未确认边界。
另外，OpenAI Astra 与 Google DeepMind 的 Project Astra 不是同一个项目。搜索时最好同时带上 OpenAI 或 GPT-6，避免把两者混在一起。
Astra 什么时候发布，ChatGPT 和 Codex 能用吗
截至 2026 年 8 月 5 日，官方状态如下：
| 用户关心的问题 | 当前答案 |
|---|
| Astra 发布日期 | 未公布 |
| 是否正式叫 GPT-6 | 未确认 |
| ChatGPT 是否可选 | 不可选，官方未宣布开放 |
| Codex 是否可选 | 不可选，官方未宣布开放 |
| API 是否可调用 | 没有公开 API model ID |
| Free / Plus / Pro 哪档可用 | 未公布 |
| Astra 价格与限额 | 未公布 |
因此，现阶段不存在可信的“Astra 充值”“Astra 激活码”或“提前开通 GPT-6”渠道。遇到要求付费获取 Astra 权限的页面，应先核对 OpenAI 官方模型目录和帮助中心，避免为尚未公开的产品付款。
如果你的目标是现在使用 ChatGPT 或 Codex，仍应按已上线模型选择。可以先看 GPT-5.6 Sol、Terra、Luna 使用指南 和 GPT-5.6 各套餐开放范围；主要使用编程代理的用户可查看 Codex 充值与开通说明。
普通用户现在该做什么
第一，不需要为了 Astra 改套餐。官方没有公布任何套餐映射，现在升级 Plus 或 Pro 只能依据当前已开放功能，不能把未来的 Astra 权限当成购买承诺。
第二，只关注三个正式信号：OpenAI 产品公告、ChatGPT 模型选择器和 API 模型文档。三者中至少出现一个明确入口后，才进入“怎么用”的阶段。
第三，区分研究能力和日常体验。数学证明展示了长程推理、搜索和形式化能力，但它不能直接证明 Astra 在写作、编程速度、中文对话、图片生成或日常问答上会提升多少。真正的使用建议要等公开版本、权限和实测数据。
本文会在 OpenAI 公布发布日期、套餐或 API 后更新原 URL，不另发近重复文章。
FAQ
Q: OpenAI Astra 是什么？
A: Astra 是 OpenAI 在 2026 年 8 月数学研究公告中首次点名的“下一代主要模型”。目前公开的只是一个内部版本的研究结果，不是已经上线的 ChatGPT 或 API 产品。
Q: Astra 就是 GPT-6 吗？
A: 官方尚未确认。Astra 可能是内部代号、模型家族名或未来产品名，现阶段不能把它直接等同于 GPT-6。
Q: Astra 什么时候发布？
A: 截至 2026 年 8 月 5 日，OpenAI 没有公布发布日期、灰度计划或候补名单。
Q: ChatGPT Plus 或 Pro 现在能用 Astra 吗？
A: 不能。OpenAI 没有宣布 Astra 对 Free、Plus、Pro、Business 或 Enterprise 中任何套餐开放。
Q: Codex 或 OpenAI API 能调用 Astra 吗？
A: 目前不能。官方没有公布 Astra 的 API model ID，也没有在 Codex 中提供模型入口。
Q: Astra 是否解决了十道未解数学题？
A: 不宜这样概括。官方称其为“十项进展”：其中 non-sofic 群构造、反例和若干 Erdős 问题属于解决长期开放问题，球堆积、编码和电路复杂度等结果则主要是推进已知边界。
Q: Astra 解决这些问题只花了 2000 美元吗？
A: 不是。约 2000 美元只指项目 token 使用量按 Sol API 费率折算的金额，不包括训练模型、人力、基础设施和学术验证成本，也不是 Astra 的定价。
Q: Lean 4 验证是否代表结果已经百分之百没有争议？
A: Lean 能机器检查形式化证明的逻辑链条，是很强的正确性证据；学界仍需核对形式化命题与原问题是否一致，并评估新颖性和意义。
Q: OpenAI Astra 和 Google Project Astra 是同一个模型吗？
A: 不是。两者来自不同公司，也属于不同项目。搜索和阅读报道时应确认页面说的是 OpenAI 还是 Google DeepMind。
参考来源
更新记录
- 2026-08-05：首发；核实 Astra 与 GPT-6 的关系、十项研究结果、Lean 4 验证边界、约 2000 美元成本口径及当前可用性。