OpenAI 周六宣布，其内部模型 "Astra" 在数学和理论计算机科学领域取得突破，成功解决了 10 项悬而未决十余年的开放性问题，并发布了可供机器验证的证明过程。

OpenAI 公开了一份 249 页的手稿合集，详细展示了模型生成的推理步骤及所有 10 个结果的 Lean 4 证书。相关代码已在 GitHub 上以 Apache 2.0 许可证开源，库中 "sorry" 计数为零，表明形式化证明中无任何步骤遗漏或未证。

攻克多项经典难题

此次最引人注目的成果是构造出一个非 Sofic 群（non-sofic group）。自 1999 年 Mikhail Gromov 引入 Soficity 概念以来，该问题一直悬而未决。尽管此前考察过的每个群均被证明为 Sofic，但无人能证明所有群皆如此，Astra 成功构建了这一反例。

此外，Astra 还推翻了 1980 年提出的 Connes 刚性猜想，构造出无穷多个具有性质 ( T ) 但共享相同冯 · 诺依曼代数的非同构群，并证明了 Ehrhart 体积猜想。在 Paul Erd ő s 目录中，Astra 解决了包括多色 Ramsey 数第 183 号问题在内的三个难题，并在极值图论中产生反例，解决了另外两个 Erd ő s 问题。其余成果涵盖高维球体堆积、二进制和球形码、算术电路复杂度、量子并行重复以及格密码学相关的最近向量问题难度。

通俗而言，群是对一组对称性的数学描述，Sofic 群结构可通过洗牌有限副扑克牌来近似。Connes 猜想则认为，对于某一类刚性群，相关代数对象充当唯一指纹以确定其来源。Astra 的发现表明，存在无穷多个共享单一指纹的不同群。

形式化验证提升可信度

Lean 证书为此次公告提供了极高可信度。Lean 内核仅给出二元裁决：证明要么编译通过，要么失败。这意味着对模型的信任不再关键，但数学家仍需确认形式化陈述是否准确反映问题实质，并评判结果重要性。目前，这 10 项成果尚未经过同行评审。

维护 erdosproblems.com 数据库的 Thomas Bloom 将 Astra 的结果称为 " 重磅新闻 "，认为其重要性超过 OpenAI 内部模型今年 5 月产生的 Erd ő s 单位距离反例。相比之下，2025 年 10 月时任 OpenAI 科学副总裁 Kevin Weil 曾声称 GPT-5 解决了 10 个 Erd ő s 问题，后被指实为检索已知文献，引发争议。

低成本与监管挑战

Astra 本身尚未发布。OpenAI 将其描述为一个旨在协调多个智能体执行复杂长程任务的模型家族，与研究科学家 Noam Brown 的测试时推理工作相关。Brown 称这些结果是 " 科学推理的重大一步 "。人类研究人员将模型输出整理为可发表论文，但 OpenAI 强调数学论证源自 Astra。

计算成本相对低廉。OpenAI 指出，按 GPT-5.6 Sol API 费率，解决这 10 个问题所需的 Token 成本约为 2,000 美元。

近日，CEO Sam Altman 向华盛顿政策制定者展示了 Astra。公司尚未公布发布日期、定价或具体命名（GPT-6 或其他 GPT-5 变体）。任何发布均需经过联邦 AI 安全审查，该流程此前已导致 GPT-5.6 延期。

这一时机对持保留态度的数学界而言颇为尴尬。今年 6 月，国际数学联盟通过《莱顿宣言》，警告 AI 公司未经同意使用研究、绕过同行评审，威胁证明和归属完整性。软件工程师 Fernando Borretti 则辩称，人类数学家的传统辩护已不再适用，领域边界将退缩至人类无法跟进的程度，" 我们将生活在一个充满我们不懂其运作原理的奇妙设备的世界。"

【星途科讯 图文丨欧阳布布 首发于 ZAKER 科技，转载请注明出处】