一句话推荐
推荐给关注AI数学、Lean形式化和研究复现的读者。PrimeGaps186是OpenAI公开的Lean 4项目与Python数值证书，用于检查“相邻素数间隔下极限不超过186”的条件性证明结构。
项目能做什么
- Lean 4形式化：项目给出DHL[40,2]、显式可容许40元组及H1≤186的形式化推导。
- 数值证书：Python脚本可重新计算优化试验和积分边界，并生成通过状态回执。
- 独立检查：仓库固定Lean和Mathlib版本，提供Lake构建、Comparator及内核检查说明。
- 研究复现：附论文、数值说明、形式化配置与Apache-2.0许可证。
重要限制
这不是完全无前提的Lean闭合证明。仓库README明确说明，形式化仍依赖三个显式输入公理：两项Deligne类型估计和一组物理积分上界。前两项在既有数学文献中有依据，但尚未在本项目中形式化；数值证书能够复算数据，却不会自动消除Lean中的公理前提。
安装与验证
git clone https://github.com/openai/PrimeGaps186.git
cd PrimeGaps186
lake exe cache get
lake build PrimeGaps186
python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json官方记录的数值环境使用Python 3.12.13、NumPy 2.2.6、python-flint 0.9.0及定制FLINT 3.6.0。直接换版本可能影响复现，运行前应完整阅读README。
适合人群
- 解析数论、素数间隔与筛法研究者
- 学习Lean 4和Mathlib的形式化数学开发者
- 研究AI如何参与数学证明与数值搜索的团队
- 需要审计“机器验证”具体覆盖范围的技术读者
关联资料
论文：
https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf
GPT-6 Astra站内导航：
https://www.zuoshipin.com/link/32152.html