OpenAI 开源 PrimeGaps186:素数间隙上界 186 的 Lean 形式化证明
johnowhitaker · x · 2026-09-04
OpenAI 发布 GitHub 仓库 PrimeGaps186,对素数间隙结果进行 Lean 4 形式化,目标是证明素数序列的下极限间隙 liminf(p{n+1}-pn) ≤ 186。
要点:
- 项目从给定输入推出 DHL[40,2]:任何由 40 个整数平移构成的可容许集合,都存在无穷多个平移同时包含至少两个素数。
- 结果是有条件的:Lean 证明依赖三条明确列出的输入公理,所引用的数学估计与数值计算尚未转化为 Lean 证明。
- 仓库附带 Python 数值证书(primegap186certificate.py)、比较器代码与数值结果 PDF。
johnowhitaker 在转发时打趣道,两小时前他的上一条回复还曾有用——暗示该结果相关的数字此前出现过波动,数学前沿进展之快令人感叹。
所属事件:GPT-6-Astra 用 Lean 证明素数间隔 ≤186，数日三破纪录(22 条相关)→
「研究」频道最新
- 斯坦福团队发布 ScholarCatalyst：检索可启发科研的先行工作 — lateinteraction · 2026-10-21
- 神经科学家 Nature 撰文：AI 没有意识，也许永远不会有 — anilkseth · 2026-10-21
- 航空业的数据溯源思路：智能体如何在图结构数据上拼证据 — 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