OpenAI｜Astra攻克10道十年未解题，配套Lean形式化证明

OpenAI没有先发一款新聊天产品，而是把下一代内部模型推进到「可核验数学」的硬场子——证明能不能过编译器，比海报上的口号更难造假。

OpenAI是美国前沿人工智能实验室，产品覆盖ChatGPT、Codex与企业级接口，研究侧持续用开放问题评估未发布模型。所谓Lean，是一种证明助手：把数学论证写成机器可检查的形式化语句，编译通过意味着在既定公理与库的前提下推导链条闭合。它不能自动裁定「这个问题在人类数学共同体里有多重要」，但能大幅压缩「看起来像证明、其实跳步」的空间。

8月1日，OpenAI发布题为「Ten advances in mathematics and theoretical computer science」的研究公告。官方称，结果由下一代主要模型Astra的内部版本取得；这些问题主结果至少十年未见进展，多数更久，覆盖高维几何、编码理论、算术电路复杂性、群论、算子代数、量子复杂性、格密码与极值组合等方向。流程上，系统生成论证，人类与同一模型整理成稿，再由模型完成Lean形式化；公司同时放出每题的推理过程叙述。官方估算，找到这10个解所需token按Sol API价格约合2000美元。OpenAI表示对正确性负责，并强调不应把完全由AI生成的证明伪造成人类独立作者成果。

十项结果方向（官方列举）：

1. 高维球体堆积：新上界下探至Cohn–Elkies阈值。
2. 二进制与球面码：在给定最小距离下指数级改进最大码规模上界，球面码有类似结果。
3. 非sofic群：构造证明非sofic群存在，回应群论中心开放问题。
4. Connes刚性猜想：反证某些群由其von Neumann代数唯一决定的长期猜想。
5. 算术电路复杂性：permanent等计算的新下界，含阶约n⁴/log n的算术公式下界。
6. 量子并行重复：一般双人量子博弈的指数并行重复定理。
7. 最近向量问题：与后量子密码相关的近似硬度结果。
8. Ehrhart体积猜想：确定各维下「质心为唯一内格点」凸体的最大体积。
9. 多色Ramsey数：多色三角形Ramsey数的超指数下界，对应Erdős问题183。
10. 极值图论猜想：紧致性与退化性相关结果，对应Erdős问题146与180。

形式化产物集中在公开仓库openai/ten-proofs：基于Lean 4.32.0、mathlib与Lake，可用lake exe cache get后执行lake build All编译全部模块，亦可按模块名单独构建。许可证为Apache-2.0。仓库还提供独立核验说明目录，方便外部研究者对照检查。

这场发布的产业含义，不在于Astra何时对公众开放——官方仍称内部版本、未给发布时间表与定价——而在于前沿实验室开始用「可机械核验的知识产物」争夺信誉，而不只是堆聊天基准分。数学共同体仍需逐题判断：形式化语句是否精确对应原问题、假设是否恰当、结果在各自领域的重要性如何。但对AI研究评价来说，「证明能否编译通过」已经把最常见的失败模式往前堵了一截。下一观察点是专业数学家的复核与跟进论文，以及其他实验室是否跟进「开放问题+形式化证书」这一发布范式。