GPT-6-Astra 用 Lean 证明素数间隔 ≤186，数日三破纪录
OpenAI 于 9 月 4 日在 GitHub 集中开源多个 Lean 形式化证明仓库，最受关注的是 openai/PrimeGaps186：由代号 GPT-6-Astra 的模型完成的 Lean 4 形式化证明，证明存在无穷多对相邻素数间距不超过 186，即素数序列下极限间隙 liminf(p{n+1}-pn) ≤ 186，对应条件性结果 DHL[40,2]。这是 GPT-6 Astra 发布后的首个科研成果，距人类刚刷新纪录仅数日，且几天内纪录被连续三次刷新，节奏之快引发数学界与 AI 界双重关注。
已确认
- 仓库已开源发布，证明由 GPT-6-Astra 完成并通过 Lean 4 形式化验证，从给定输入推出 DHL[40,2] 条件性结论；据机器之心报道，该成果以论文形式发布，由 OpenAI 研究员、宾大教授苏炜杰宣布，论文题为《Improved Short Ga…》（题目在转述中被截断）
- 据 @NoFaithlessness951，OpenAI 的 GitHub 同批出现多个新仓库，还包括 openai/LongGapsBetweenPrimes、openai/ten-proo 等，被社区解读为为 Astra 铺路
- 据 @scaling01 与 @johnowhitaker 转述，此前最佳上界 240 由 Julia Stadlmann 于 8 月 31 日刚发表，随即被刷新
- @teortaxesTex 补充时间线：人类纪录为 2014 年 Polymath 协作项目的 246，随后 Stadlmann 证明 240、AxiomMath 给出 212，两天内纪录三连破，GPT-6-Astra 最终刷到 186
- 据 @新智元梳理的更长脉络：2013 年张益唐证明间距小于 7000 万，Maynard 等随后推进，246 的纪录由陶哲轩参与的 Polymath 项目保持约 12 年，三天内三破；量子位也作了类似梳理
- 被 @scaling01 引用的 @AcerFur 说明：结果以 186 为条件，是因为其依赖 Deligne 相关条件
- @weijie444 与量子位将其表述为孪生素数猜想相关问题上界从 246 推进到 186，并提到该方向与张益唐 2013 年突破一脉相承
- 据 @burnytech 转述，此前数周 Jack Kleeman 与 Claude 已将 Goldston 的结果形式化为 186 的前身工作，形式化验证此领域本就活跃
- 据 @raphagl 与 @ChrSzegedy 转述的发布活动内容，配套的素数最大间隔（长间隙）结果由数学家 Mehtaab Sawhney 宣布，将上界缩小约一个 log log n 因子，被称为 1930 年代以来该量级的首个改进
- 据 @teortaxesTex 转发的数学圈评价，LongGapsBetweenPrimes 结果证明极其初等却似被所有解析数论学家漏掉，Lean 形式化仅约 4500 行代码，是当前 SOTA，改进了 Erdős 问题 4 的纪录
- 据 @scaling01 转述 Noam Brown 的表态：在 GPT-6 Astra 的众多用途中他最看好科学发现，并称 OpenAI 尚未在该模型的数学与科学能力上压榨到极限
尚未确认
- GPT-6-Astra 的具体身份、能力边界及正式发布时间均未由 OpenAI 官方说明，「为 Astra 铺路」仅是社区解读
- @新智元另报道称 OpenAI 已发布代号 Astra 的 GPT-6，Greg Brockman 称「历史会证明就是这个模型」，官方博客文章一度 404、目前仅向部分用户开放；该报道细节高度反常，真实性未经证实，需谨慎对待
- 长间隙结果「1930 年代以来首个改进」的说法来自转发转述，尚待一手文献核实
为什么重要
- 这是前沿大模型独立产出并通过严格形式化验证的数论成果，方向与张益唐 2013 年有界素数间隔突破一致，展示 AI 在正式数学证明上的能力
- 人类保持约 12 年的 246 纪录刚被刷新（240）数日之内，纪录先被推至 212 再到 186，速度罕见；配套长间隙结果若坐实为 1930 年代以来首个量级改进，意义更为重大
- 证明以 Lean 形式化并开源，可被社区检验、复用；Noam Brown 的表态也暗示 OpenAI 将科学发现作为模型重点方向
2026-09-04 ~ 2026-09-04 · 22 条相关
一手来源
- OpenAI 开源仓库:GPT-6-Astra 用 Lean 形式化证明素数间隔 ≤186 — scaling01 ·
- OpenAI 开源 PrimeGaps186:素数间隙上界 186 的 Lean 形式化证明 — johnowhitaker ·
- GPT-6 Astra 将素数间隔上界从 246 推进至 186 并过 Lean 验证 — 机器之心 ·
- 【源头】OpenAI 开源仓库:GPT-6-Astra 用 Lean 形式化证明素数间隔 ≤186 — scaling01 · 2026-09-04
- GPT-6-Astra 形式化证明素数间隔上界 186，此前纪录 240 仅为数日前 — scaling01 · 2026-09-04
- 【源头】OpenAI 开源 PrimeGaps186:素数间隙上界 186 的 Lean 形式化证明 — johnowhitaker · 2026-09-04
- OpenAI 官方账号连发素数证明仓库,被指为 Astra 铺路 — NoFaithlessness951 · 2026-09-04
- 素数间隔纪录两天内三连破,GPT 6 Astra 刷到 186 — teortaxesTex · 2026-09-04
- AI 辅助证明仅 4.5k 行 Lean 代码，刷新 Erdős 问题 4 纪录 — teortaxesTex · 2026-09-04
- Noam Brown:GPT-6 Astra 用 Lean 证明有界素数间隔,最看好科学发现用途 — scaling01 · 2026-09-04
- OpenAI 称 GPT-6 Astra 将孪生素数间隙从 246 推进到 186 — weijie444 · 2026-09-04
- 曝 OpenAI 发布 GPT-6 Astra:素数间隔破 90 年纪录,官方博客曾短暂 404 — 新智元 · 2026-09-04
另有 13 条近重复转述:scaling01 · scaling01 · scaling01 · burny_tech · weijie444 · rapha_gl · weijie444 · Singularitarian · khademinori · 量子位 · 新智元 · ChrSzegedy · 机器之心