OpenAI Astra：数学与理论计算机科学领域的十项进展

OpenAI Astra 解决了十个长期存在的数学问题

OpenAI 宣布，其下一个重大模型 Astra 的内部版本已成功解决了数学和理论计算机科学领域的十个开放性问题。这些问题的主干结果至少十年没有进展，在许多情况下，时间甚至更长。为了确保正确性，OpenAI 已通过公开的 GitHub 仓库为每个证明发布了 Lean 证书。

数学突破摘要

这些结果涵盖了多个复杂的领域，包括高维几何、群论和量子复杂度。解决的十个问题包括：

• 高维球体填充： 建立了新的球体填充密度的上限，直至达到 Cohn–Elkies 阈值。
• 二进制与球面编码： 在任何指定的最小距离下，对二进制编码的最大规模产生了指数级的改进界限，高维球面编码也有类似的结果。
• 非 sofic 群： 提供了一种构造方法，证明了非 sofic 群的存在，解决了群论中的一个核心开放问题。
• Connes 刚性猜想： 驳回了某些群由其 von Neumann 代数唯一确定的猜想。
• 算术电路复杂度： 建立了使用算术电路和公式计算 permanent 的新下界，包括一个 $n^{4/\log n}$ 阶的算术公式下界。
• 量子并行重复定理： 为通用的双人量子博弈开发了一个指数级的并行重复定理，扩展了经典复杂度理论的原则。
• 最近向量问题： 发现了最近向量问题的多项式因子近似难度，这是后量子密码学中的一个关键格问题。
• Ehrhart 体积猜想： 确定了在每个维度下，质心为其唯一内部格点的凸体的最大可能体积。
• 多色 Ramsey 数： 通过为多色三角形 Ramsey 数提供一个超指数下界，解决了 Erdős 问题 183。
• 极值图论猜想： 通过解决关于极值图论中紧凑性和退化性的 Erdős 问题 146 和 180，解决了极值数猜想。

方法论与资源消耗

这些解决方案是由 Astra 模型的内部版本生成的。OpenAI 报告称，按目前的 Sol API 费率计算，寻找这些解决方案的总 token 成本约为 2,000 美元。

在 AI 发现数学论证之后，人类研究人员与模型协作，将结果整理成手稿。最后，模型将每个论证形式化为 Lean 证书，以提供机器可验证的正确性证明。

AI 数学领域的责任与归属

OpenAI 断言，归属应当诚实地反映结果的来源，并表示声称 AI 生成的证明为人类原创将误导知识工作的本质。虽然人类在手稿准备和 Lean 形式化过程中提供了协助，但 OpenAI 将核心数学论证归功于 Astra 系统。

社区分析与反论点

该公告在技术社区内引发了关于 AI 驱动的发现以及过程透明度的重大辩论。

透明度与实验严谨性

一些批评者认为，如果没有实验设置的完全透明，报告的 2,000 美元成本可能会具有误导性。

"I want to know: 1. How many total problems were given to the model, and what percent were left unsolved at what cost before giving up? 2. How many attempts did you give the model at solving these problems?"

启发式搜索 vs. 新颖理论

目前正在讨论模型是在生成真正新颖的数学理论，还是仅仅在对现有工具进行穷举搜索，以寻找已知问题的正确组合。

"Do these proofs contribute new ideas to the mathematical corpus, or are they simply an effective method to exhaustively search the literature for the right combination of existing tools to apply to the problem?"

技术观察

观察者注意到，其中一些生成的 Lean 证明非常长——长达 50,000 行——这突显了 AI 生成的形式化证明与简洁的人类编写的证明之间的区别。

对数学专业的影响

虽然有些人将这些结果视为对该专业的威胁，但其他人认为 AI 将起到催化剂的作用，为人类研究人员开辟新的途径。

"For every conjecture defeated some seven or eight new ideas open up. Our path through that combination will be set by creative and curious human mathematicians."