OpenAI 新仓库：模型以 Lean 形式化证明素数间隔上界 186
scaling01 · x · 2026-09-04
scaling01 分享了 OpenAI 的一个新代码仓库，其中标注为由 GPT-6-Astra 完成的 Lean 形式化证明，证明了存在无穷多对相邻素数，其间距不超过 186。这与张益唐 2013 年“有界素数间隔”突破的方向一致，但上界更小、结论更强，若属实展示了前沿模型在形式化数学领域的快速进步。不过帖子未给出 OpenAI 官方说明，GPT-6-Astra 的具体身份也尚待证实，建议保持关注。
所属事件: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