GPT-6 将孪生素数上界压至 186，陶哲轩守 12 年的纪录三天三破
新智元 · wechat · 2026-09-04
OpenAI 宣布 GPT-6（Astra）把孪生素数猜素的最好上界从 246 推进到 186，并开源了 Lean4 形式化验证仓库 PrimeGaps186。
- 纪录时间线：2013 年张益唐证明间距小于 7000 万，Maynard 与陶哲轩的 Polymath 项目压到 246；2026 年 8 月 31 日牛津数学家 Julia Stadlmann 推到 240，9 月 3 日早晨 Axiom Prover 宣布 212，仅数小时后 OpenAI 发布论文给出 186。
- 方法突破：GPT-6 提出新的「三重稠密可除性」条件，放宽了对平滑模数的限制，在 Selberg 筛法中扩展权重支持，构建出 40 元素、直径 186 的可容许集合。
- 形式化验证：证明配有可执行的 Lean4 代码与数值证书，但有三条依赖有限域指数和估计（如 Deligne 定理）的输入公理尚未在 Lean 中形式化，属「有条件」证明。
- CoT 记录：GPT-6 展现出纠错与科研品味——拒绝定性元组的捷径、放弃浮点近似改用精确有理数算术、在 41 维优化死胡同时改用不对称密度分配策略在 40 维架构下让积分比值超过 1。
OpenAI 研究员苏炜杰称这是「见证一个新智能时代诞生」；UC 伯克利 Tony Feng、弗吉尼亚大学 Ken Ono 等数学家均高度评价。距终极目标「2」仍有距离，但 AI 已从辅助工具变为数论前沿发现者。
所属事件:GPT-6-Astra 用 Lean 证明素数间隔 ≤186，数日三破纪录(22 条相关)→
「研究」频道最新
- 航空业的数据溯源思路：智能体如何在图结构数据上拼证据 — colinmcnamara · 2026-10-21
- SFT 阶段配方公开:指令/推理/代码/数学混训,不做多 epoch — TimDarcet · 2026-10-21
- 训练中期阶段揭秘:扩到 131k 上下文,「不要 logit,只要 token」 — TimDarcet · 2026-10-21
- 数学家 Daniel Litt 认输后谈 AI：能解题，但自动化不了数学研究 — ziv_ravid · 2026-10-21
- AI 制药真实现状：不是一句话治癌，而是海量结合筛选加毒性过滤 — burny_tech · 2026-10-21
- PyTorch 官方详解 IBM Spyre 后端：KTIR 与数据流调度器如何跑通 AI 加速器 — PyTorch · 2026-10-21