GPT-6 Astra 被归因于将有界素数间隔纪录推进至 186

发生了什么？

OpenAI 在 2026 年 8 月 30 日发布的预印本声称 GPT-6 Astra 找到了一项证明， 建立 DHL[40,2]；将其应用于一个直径为 186 的显式 admissible 40-tuple，可得到 连续素数间隔满足 liminf_(n->infinity)(p_(n+1)-p_n) <= 186。该结果改进了 Polymath8b 对应的 246 纪录，并比 Julia Stadlmann 独立得到的 240 上界早一天发布。

公开的 PrimeGaps186 仓库包含 DHL[40,2] 与 186 素数间隔结论的 Lean 4 开发， 并附带 Python/FLINT 数值 certificate。登记的主要 Lean declaration 均无 sorry， OpenAI 报告 Comparator、Nanoda 与 Lean kernel 均接受这些条件式证明。但形式化 仍依赖三个显式项目公理：一个 rank-three hyper-Kloosterman 估计、一个 rank-two Kloosterman correlation 估计，以及一组 physical-integral 与 cap bounds。前两个 输入来自既有文献；数值输入由配套 certificate 检查，而没有在 Lean 内证明。 OpenAI 自身的 metadata 将审查状态标为 self-assessed，并明确说明尚无独立人类 semantic review。

为什么重要？

有界素数间隔问题是现代素数分布研究中最知名的持续推进路线之一。在约十二年后把公开 无条件纪录从 246 推进至 186，本身就具有显著数学意义；而证明又被公开归因于前沿 AI 模型，使该事件成为 AI 系统直接贡献新前沿数学的代表案例。配套形式化同时清楚展示一种 新的验证边界：机器检查可以强力验证庞大的条件式推导，但被引用的数学估计和数值输入 仍可能位于 proof assistant 之外。

重要性说明：该结果被列为 Historical Milestone，因为它不是 benchmark 提升或对已知数学的重新 形式化，而是一个被归因于 AI 的解析数论前沿推进。OpenAI 预印本声称得到 liminf(p_(n+1)-p_n) <= 186，把 Polymath8b 长期保持的 246 上界进一步降低； Terence Tao 的 Optimization Problems 记录把 186 列为当前最好已知上界，并注明 246 纪录保持了十二年。该成果同时提供大规模 Lean 与数值验证产物。这里的历史 重要性与数学输入及 provenance 仍未完全验证的状态严格分开记录。

历史脉络

主要证据

• Improved short gaps between primes
  S1 · 主要研究来源 · 论文 · 2026-08-30
• Prime Gaps at Most 186
  S1 · 主要研究来源 · 代码仓库
• PrimeGaps186 formalization metadata
  S1 · 主要研究来源 · 形式化工件