PrimeGaps186 README

The project's README from github.com/openai/PrimeGaps186. As one markdown file: README.md.

Prime Gaps at Most 186

This repository contains a Lean 4 formalization of a prime-gap bound and a Python numerical certificate. The Lean results remain conditional on three explicit input axioms; the cited mathematical estimates and numerical computations have not been turned into Lean proofs of those inputs.

The result

For the sequence of primes $p_n$, the target bound is

\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186.

The development derives $\mathrm{DHL}[40,2]$ from the inputs below: every admissible set of forty integer shifts has infinitely many translates containing at least two primes. Admissibility means omitting a residue class modulo every prime. Applying this to the included tuple of diameter 186 gives the gap bound.

The main declarations in PrimeGaps186.lean, in namespace PrimeGap186, are:

Declaration Result
dhl_40_2 $\mathrm{DHL}[40,2]$ for every admissible integer tuple.
infinite_two_prime_translates_admissibleTuple Infinitely many two-prime translates of the explicit tuple.
primeGapLiminf_le_186 The consecutive-prime gap bound.

Assumed Deligne-type estimates

For a prime $p$, write $e_p(x)=\exp(2\pi i\widetilde{x}/p)$, where $\widetilde{x}$ is any integer representative of $x\in\mathbb{F}_p$. Define

\mathrm{Kl}_3(c;p)
=\frac1p\sum_{\substack{x_1,x_2,x_3\in\mathbb{F}_p\\x_1x_2x_3=c}}
e_p(x_1+x_2+x_3),

K_2(c;p)=\sum_{u\in\mathbb{F}_p^\times}e_p(u+c/u).

The axiom PrimeGap186.kloosterman3_bound assumes the following bound for every prime $p$ and all $c\in\mathbb{F}_p^\times$:

\left|\mathrm{Kl}_3(c;p)\right|\le 3.

This follows from Deligne's theorem as stated in Nicholas M. Katz, Gauss Sums, Kloosterman Sums, and Monodromy Groups, Annals of Mathematics Studies 116, Princeton University Press (1988), Theorem 4.1.1(1)–(2), p. 49. With $n=3$, trivial multiplicative characters, and $b_1=b_2=b_3=1$, rank three and weight two give the raw bound $3p$; our normalization divides by $p$.

The axiom PrimeGap186.kloosterman2_correlation_bound assumes the following bound for every prime $p$ and all $A,B\in\mathbb{F}_p^\times$:

\left|\sum_{t\in\mathbb{F}_p\setminus\{0,-1\}}
K_2(A/t;p)\,K_2(B/(t+1);p)\right|\le 8p\sqrt p.

This is Étienne Fouvry, Emmanuel Kowalski, and Philippe Michel, The Friedlander–Iwaniec character sum, 14 June 2013, Proposition 2, p. 1. Their normalized $\mathrm{Kl}_2(c)$ equals $K_2(c;p)/\sqrt p$ after inverting the summation variable, so their $8\sqrt p$ bound becomes $8p\sqrt p$ here. No condition $A\ne B$ is imposed; the two poles are excluded even when $A=B$.

These estimates are established in the cited literature, but remain unproved inputs in this Lean development.

Numerical input and certificate

PrimeGap186.physical_integral_bounds assumes 104 outer and 45 inner physical-integral upper bounds, plus three cap bounds.

The Python certificate recomputes the trial from scratch. The tested environment used Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0, and a custom FLINT 3.6.0 build with corrected signed polynomial convolution (not bundled).

python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json

Use a new output path. Keep PYTHONOPTIMIZE unset and do not use -O or -OO. Mandatory floating-point and signed-convolution checks must pass. A successful run produces a receipt with passed: true; it does not discharge any Lean axiom.

Building and verification

The project pins Lean 4.34.0-rc2 and its Mathlib dependencies. With elan installed, run:

lake exe cache get
lake build PrimeGaps186

The registered Lean build passed without errors or warnings. Comparator matched all three results to Challenge.lean, and Nanoda and Lean’s kernel accepted their proofs in a local Colima Linux VM. The configuration permits the three documented project axioms plus propext, Quot.sound, and Classical.choice (six total); this verifies conditional proofs, not the inputs themselves. The numerical certificate is unchanged from its earlier passing run.

Challenge.lean specifies the statements and input assumptions, with three intentional theorem placeholders. See the Comparator instructions and formalization metadata for the checking setup and status.

Project contributions use Apache 2.0; existing third-party notices remain applicable.

PrimeGaps186 (openai/PrimeGaps186)

Searching Database…

167 ·GitHub
PrimeGaps186
这是什么？这是一个 Lean 4 形式化项目，证明相邻素数间隙的一个上界（间隙至多 186），并附带一个 Python 脚本，对证明所用的输入进行数值验证。
这是完整的数学证明，还是仍依赖未证实的假设？Lean 证明从三条显式公理（两个 Deligne 型估计和一组数值界）推导出间隙上界，这些公理引自已发表论文，但并未在 Lean 内部自行证明。
怎么构建并验证它？安装 elan，然后运行已注册的 Lean 构建，它会锁定 Lean 4.34.0-rc2 及其 Mathlib 依赖；结果使用 Comparator 工具对照 Challenge.lean 进行检查。
运行 Python 数值证书需要什么？你需要 Python 3.12.13、NumPy 2.2.6、python-flint 0.9.0，以及一个带有修正带符号多项式卷积补丁的自定义 FLINT 3.6.0 构建（仓库中不包含）。
通过数值证书就等于证明了定理吗？不是——数值证书运行成功只能确认数值输入能正确复算，并不能解除 Lean 公理，因此整体结果仍是有条件的。
实际谁会用这个仓库？它面向解析数论和形式化验证领域、想检查或扩展特定素数间隙上界的有条件证明的研究人员，而非一般开发者。
Lean 构建实际是在什么环境测试的？Lean 构建和内核检查是在本地 Colima Linux 虚拟机中运行并验证的，Nanoda 和 Lean 内核均接受了这些证明。
DHL[40,2] 具体是什么？它为什么重要？DHL[40,2] 指出：任何由 40 个整数平移构成的容许集都有无穷多个平移版本至少包含两个素数；把它应用于一个直径 186 的特定元组，就得到相邻素数间隙的上界。
证明依赖的三条公理是什么？其中两条是 Deligne 型 Kloosterman 和上界（kloosterman3bound 和 kloosterman2correlationbound），引自 Katz 的专著和一篇 Fouvry-Kowalski-Michel 论文；第三条（physicalIntegralBounds）是 104 个外层和 45 个内层数值积分界，外加三个 cap 上界。
Challenge.lean 是什么？该文件把目标命题和输入假设指定为三个有意留下的定理占位符，Comparator 工具用它来检查主 Lean 文件是否确实证明了这些命题。
经验证的构建总共依赖多少条受信公理？六条：三条项目特定的输入公理，外加标准的 Lean/Mathlib 公理 propext、Quot.sound 和 Classical.choice。
What are similar projects?fermats-last-theorem, integer-mult-bounds, math, NavierStokesAndEuler, XRAG, fluid_lean, wikiskill, OpenWAM
Which topics is it in?lean, arxiv, mathematics, academic-research, research, apache-2.0, python, cross-platform, windows, macos, linux
Creator
openai
Size
2.2 MB
Stars
167
Updated
CommitSep 02
Age
1mo
Commits · 90 Days