OpenAI表示，旗下尚未公开的内部模型Astra已在数学、量子复杂性和理论计算机科学领域取得突破，针对10个悬而未决至少10年的问题给出新结果，并同步公开了可机器验证的形式化证明。

据SiliconANGLE等外媒2日（当地时间）报道，OpenAI已在GitHub上以Apache 2.0许可证开源一份249页的论文草稿、模型生成的推理过程，以及基于Lean 4的证明证书。公开仓库显示，证明文件中的“sorry”为零。OpenAI解释称，这意味着相关形式化证明中不存在未完成步骤。

此次公布的代表性成果包括：自Mikhail Gromov于1999年提出索菲克性概念以来长期悬而未决的“非索菲克群的显式构造”问题。OpenAI还称，Astra为Alain Connes于1980年提出的强刚性猜想给出了反例，构造出无限多个彼此不同的性质(T)群，而这些群对应同一个冯·诺伊曼代数。

此外，OpenAI表示Astra还证明了Ehrhardt的体积猜想，并称解决了Paul Erdős问题列表中的3个问题，其中包括与多色拉姆齐数相关的第183号问题。

OpenAI介绍，索菲克群是指可由有限置换近似的一类群。迄今为止，研究者接触到的所有群都被认为是索菲克群，但“是否所有群都是索菲克群”仍未得到证明。Astra此次给出的结果，意味着这一长期存在的判断可能存在例外。

对于Connes猜想，OpenAI进一步解释称，传统设想认为相关代数对象能够唯一识别原始群结构，而Astra构造出的结果表明，无限多个不同的群可能对应同一个代数“指纹”。

其余结果还涉及高维球填充、二元编码与球面编码、算术电路复杂度、量子并行重复，以及最近向量问题（CVP）的困难性等方向。CVP与格密码研究密切相关。OpenAI还称，Astra在极值图论中给出一个反例，并额外解决了2个Erdős问题。

OpenAI强调，此次发布的关键在于Lean 4证明证书。由于Lean内核会以“通过或不通过”的方式验证证明是否可编译，因此在形式化验证层面，外界无需直接相信模型的文字表述。不过，每一条形式化陈述是否准确对应原本的未决问题，以及这些结果究竟具备多大数学意义，仍有待学界进一步核验。目前，这10项成果也尚未经过同行评审。

OpenAI过去曾因类似表述引发争议。2025年，时任科学副总裁Kevin Weil曾宣称GPT-5解决了10个Erdős问题，但Erdős问题数据库运营者Thomas Bloom批评这一说法是“戏剧性的扭曲”。当时，相关模型被指仅停留在检索既有论文层面，Kevin Weil随后删除了相关帖子。Google DeepMind CEO Demis Hassabis也将其称为一个令人尴尬的案例。

不过，这一次外界评价出现了变化。Thomas Bloom表示，Astra此次的结果是“重大新闻”，而且相比他此前参与核验的OpenAI内部模型在今年5月给出的Erdős单位距离问题反例，又向前迈进了一步。

Astra目前仍未对外发布。OpenAI介绍称，这一家族模型的设计目标是支持多智能体长期协作完成复杂任务，也是研究科学家Noam Brown主导的测试时推理研究的延伸。Noam Brown在X（原Twitter）发文称，这是“科学推理的重要进展”。OpenAI同时表示，虽然最终论文由人类研究者整理成文，但核心数学论证本身由Astra生成。按GPT-5.6“Sol”API定价估算，这10个解法的token成本约为2000美元。

OpenAI CEO Sam Altman近期已在华盛顿向政策制定者演示Astra。不过，OpenAI尚未决定该模型的发布时间、定价方案，以及是否会将其纳入GPT-6。即便最终发布，Astra仍需通过联邦层面的人工智能安全审查，这一流程也曾导致GPT-5.6延期。

与此同时，国际数学联盟支持《莱顿宣言》，并警告人工智能企业存在“未经同意使用公开研究、绕开同行评审，以及威胁证明与作者署名完整性”的风险。软件工程师Fernando Borretti则认为，人类数学家现有的防御逻辑可能不再适用，AI或将改变数学研究的最前沿。

随着Astra此次成果公开，相关讨论已不再局限于技术本身。学界将以何种标准核验并接纳AI生成的数学结果，以及如何建立相应的版权和科研伦理框架，正成为新的争议焦点。