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 在转发时打趣道,两小时前他的上一条回复还曾有用——暗示该结果相关的数字此前出现过波动,数学前沿进展之快令人感叹。
所属事件:OpenAI开源Lean仓库：GPT-6-Astra证明素数间隔≤186(9 条相关)→
「研究」频道最新
- 矩阵即图,图即矩阵:被低估的线性代数核心洞察 — TivadarDanka · 2026-09-04
- 仿真物理失真让机器人学到现实世界行不通的操作技巧 — binarybits · 2026-09-04
- 机器人操控任务为什么难靠仿真训练?一篇机器人数据调查讲透行业现状 — binarybits · 2026-09-04
- 谷歌研究：迁移学习提升低代表性人群的基因组预测 — Google Research · 2026-09-04
- 研究称标准 AI 基准测试系统性低估能力,多模型路由错误率降 46% — CodeByPoonam · 2026-09-04
- davidad 提出猜想：多 AI 交叉奖励与 self-DPO 共享同一机制原理 — davidad · 2026-09-04