### [PrimeGaps186 – OpenAI开源的素数间隔186条件性Lean证明项目](https://www.zuoshipin.com/)

**Published:** 2026-09-04T14:00:38

**Author:** 天才交易员

**Excerpt:** OpenAI开源的Lean 4条件性形式化与Python数值证书项目，用于检查素数间隔H1≤186的证明结构、…

## 一句话推荐

**推荐给关注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](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf)

**GPT-6 Astra站内导航：**  
[https://www.zuoshipin.com/link/32152.html](https://www.zuoshipin.com/link/32152.html)



---