OpenAI 用 Lean 4 证明素数间隙不超过 186

GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186

OpenAI 在 GitHub 上开源了 PrimeGaps186 项目，利用 Lean 4 对素数间隙上界进行了形式化验证。该研究证明了连续素数之间的最小间隙极限不超过 186，即存在无穷多对间距在 186 以内的素数。项目包含 Lean 4 的形式化证明和 Python 数值证书，但核心推导依赖于三个未完全证明的输入公理，包括 Deligne 型估计和特定的数值积分界限。尽管这些数学估计在文献中已有记载，但在当前的 Lean 开发中仍作为假设条件存在。通过 Python 脚本重新计算生成的证书验证了数值部分的正确性，而 Lean 构建过程也通过了无错误检查。这一工作展示了形式化验证在复杂数论问题中的应用潜力，同时也揭示了自动化证明系统中对基础数学定理依赖的边界。