post cover

AI 热点快报：OpenAI 内部模型 Astra 一役解决 10 个开放数学难题（2026-08-04）

事件与背景

美东时间 8 月 3 日（北京时间 8 月 4 日凌晨），OpenAI 发布公告《Ten advances in mathematics and theoretical computer science》（数学与理论计算机科学的十项进展），宣布其下一代内部模型 Astra 在纯数学与理论计算机科学中解决了 10 个开放问题。按官方表述，这些结果「由 Astra 的一个内部版本取得，Astra 是我们的下一代主要模型」——这是 OpenAI 第一次用「可机器验证的研究级成果」来为下一代旗舰模型做能力宣告：所有结果都不是模型自说自话，而是全部配套了 Lean 4 形式化证明证书，开源在 GitHub 仓库 openai/ten-proofs 中（仓库 8 月 1 日创建，发布当天即获得 400+ star、40+ fork），并同步放出完整论文 PDF 与一份由 AI 模型阅读原始思维链后撰写的「推理复盘」文档。消息在 Hacker News 上拿到 497 分、760+ 条评论，是当日讨论最激烈的技术事件。

这份成果并非孤立出现。The Decoder 的报道指出，过去几周数学界已被 AI 连续冲击：OpenAI 此前对 Erdős 单位距离猜想的反驳引发了连锁反应，Fields 奖得主 Timothy Gowers 公开表示 GPT-5.6 Pro 曾一次尝试就解决了他长期钻研的两个问题，Epoch AI 的 FrontierMath 开放问题集也迎来第二个被 AI 解出的题目。Astra 的 10 项进展相当于把「AI 能解开放数学问题」从个案升级为成体系的能力宣言。

10 个结果的具体清单（来自论文 PDF）：

  1. 高维球堆积：精确确定了 Cohn–Elkies 线性规划的指数增长速率，改进了高维一般堆积上界；
  2. 二进制码与球面码：在所有参数范围内将经典固定距离上界改进指数级；
  3. 非 sofic 群：构造出显式非 sofic 群，回答了「每个可数群是否都有有限置换逼近」这一群论开放问题；
  4. Connes 刚性猜想：构造无穷多个互不同构的 property-(T) 群却具有相同的群 von Neumann 代数，给出反例；
  5. 算术电路复杂度：permanent 的无除法电路下界 Ω(n² log log n)、公式下界 Ω(n⁴/log n)；
  6. 量子并行重复：对任意有限双人纠缠博弈证明指数级并行重复定理；
  7. 最近向量问题（CVP）：从 3SAT 归约得到 n^1/400 因子近似硬度；
  8. Ehrhart 体积猜想：证明每个维度凸体的最大体积上界 (n+1)ⁿ/n!；
  9. 多色 Ramsey 数：证明 R_k(3) = k^Θ(k) 超指数下界，解决 Erdős 问题 183；
  10. 极值图论：构造二分图反例反驳 Erdős–Simonovits 紧致性猜想与 Erdős 退化猜想，解决 Erdős 问题 146 与 180。

来源：

为什么现在重要

1. 「可验证性」第一次成为模型能力的核心卖点。 此前 AI 写代码、写文章都可能出错，读者无法区分「真懂」与「幻觉」。Astra 的这 10 个结果全部有 Lean 4 机器可检查的证明证书——任何一个学过形式化验证的人都可以独立复现验证，幻觉风险被从结果中剥离。更值得注意的是，OpenAI 连「推理复盘」文档都交给 AI 撰写，并公开了用 Comparator 工具做独立检查的入口，整个发布刻意强调「可独立验证」而非「我们很厉害」。影响判断：模型评估的基准正在从「benchmark 分数」转向「能否产出可验证成果」，这对所有做 AI 评估、做 Agent 质量门禁的团队都是一次方法论冲击。

2. 问题含金量不是玩具题。 两个 Erdős 问题（183、146/180）、Connes 刚性猜想（算子代数领域的核心开放问题）、非 sofic 群构造（悬置数十年的群论问题）——这些是数学家几十年没有解决的硬问题，不是合成 benchmark。尤其 Connes 刚性猜想的反例涉及「群 von Neumann 代数」这一算子代数核心对象，业界普遍认为这类结果需要深度领域直觉。影响判断：AI 在数学上的角色从「辅助计算器」进入「独立研究者」区间，研究工具、基金评审、论文发表的定价逻辑都会被重估。

3. 工程界「AI 不可信」叙事被撕开一个口子。 一线工程师对 LLM 最大的抱怨是「输出无法保证正确」。Astra 给出的答案是：让模型输出形式化证明，用证明助手锁死正确性。这个模式一旦被验证可行，就可以平移到代码生成（类型系统即证明器）、配置生成（schema 校验）、数据分析（可复现脚本）等一切「产出可检查」的场景。影响判断：Agent 工具链会加速集成 Lean/mathlib 这类证明助手作为「推理检查器」，CI 里跑「生成 + 机器验证」会成为高质量 Agent 的标配。

4. 数学界的反应分裂本身就是信号。 Fields 奖得主 Timothy Gowers 警告这可能带来「数学文化的毁灭」；伦敦玛丽女王大学数学教授 Abhishek Saha 则说前沿模型「至少相当于一个勤奋且不知疲倦的 PhD 学生」，他自己花一整天用 GPT-5.5 Pro 做完了过去要几周的常规工作，角色从「演奏者」变成「指挥」。就连长期唱衰 AI 的批评者 Gary Marcus 也罕见地在评论中承认：Astra「令人惊叹，这一点无可否认」。Gowers 的担忧本质是：如果下一代数学家不再亲手构建证明所需的概念直觉，数学社区会失去理解这类成果的能力。影响判断：数学家、基金评审、同行评议流程都会围绕「AI 参与的证明」重构，相关治理与教育讨论会持续升温。

5. 与开源路线的对照更加鲜明。 昨天（8/3）的新闻是阿里 Qwen3.8-Max 开源 2.4T 旗舰权重，今天 OpenAI 用「未发布的 Astra + 可验证推理」回应。一个主打权重开放、一个主打能力上限与可验证性，两条路线的产品叙事已经清晰分化。对做选型的团队来说，这不再是「闭源更强 vs 开源更省」的简单二分，而是「谁的能力可被验证、可被审计」的新维度。影响判断：企业级采购的评估表上，「可验证输出」将成为与跑分、成本并列的第三根支柱。

工程师/产品人今天能做什么

  1. 复现验证： 拉取 openai/ten-proofs 仓库（需要 Lean 4.32 + mathlib，用 elan 管理工具链），依次执行 lake exe cache get 与 lake build All，1 小时内可以亲眼看到 10 个机器可检查的证明证书如何构建——这是理解「可验证 AI」最直接的动手路径，也是向团队证明「AI 产出可被机器锁定」的最佳演示素材。
  2. 改造自己的 Agent 流水线： 把「LLM 生成 → 自动检查」当作默认模式：关键输出接类型检查、property test、contract 或全量单测，让机器验证成为产出的一部分，而不是事后人工 review。先挑一个高频场景（比如 SQL 生成、配置文件生成）试点「生成 + 验证循环」，跑通后再推广。
  3. 关注证明助手生态： 装 elan + Lean 4，跑一遍推理复盘 PDF 里记录的思路过程，评估「LLM 出思路 + 证明助手把关」的工具链是否值得纳入团队技术栈。形式化验证不再只是学术圈玩具，它正在成为「AI 可信输出」的基础设施。
  4. 更新评估指标： 给模型选型增加「可验证产出」维度——不只看 benchmark，看模型能否产出能通过 CI 的补丁、证明或测试用例；这比任何跑分都更能预测生产环境表现。可以先把「修复后能否通过全量单测」设为内部模型对比的硬性门槛。
  5. 跟踪 Astra 发布节奏： 留意 OpenAI 何时把 Astra 开放到 API；一旦可用，优先用数学/推理/形式化任务做小范围实测，判断下一代推理能力是否值得升级。同时留意其定价与限流策略，评估是否影响现有模型路由方案。

待观察

  1. 实验透明度： HN 顶评质疑 OpenAI 只公布了成功的 10 题，未披露总共尝试了多少问题、成功率与单题成本（社区流传的「单题 $2000」说法只是评论中的假设性讨论，尚无可靠来源证实）。若后续公布失败样本与总预算，将是对「AI 科研能力」更完整的一手数据，也会直接影响「AI 证明是否划算」的商业判断。
  2. 同行复核： 10 个证明是否全部通过独立专家与 Lean 社区复核——仓库里已经随附 ComparatorChallenges 目录，OpenAI 邀请第三方用 Comparator 工具独立挑战这些形式化证书；有没有证明在复核中被发现漏洞或被撤回，这是判断含金量的关键后续节点。数学界对「AI 证明」的接受度，很大程度上取决于这批证书能否经得起挑剔的同行审阅。
  3. 开源阵营跟进： HN 讨论中提到 DeepSeek 声称证明了 Ziegler 交叉多胞形猜想（对应 arXiv 链接本机未能访问验证），开源模型能否复现同类「可验证数学成果」、以多快速度跟进，将决定「可验证推理」是闭源专属还是普惠能力。若开源模型也能产出 Lean 证书，形式化验证基建将迎来真正的生态爆发。