Bounded gaps between primes

DefinitionSubpower bound#✓fully proved

For functions \(f, g : \mathbb{R} \to \mathbb{R}\), \(f\) is bounded by \(g\) up to subpower losses if for every real \(\delta > 0\) we have \(f(x) = O(x^{\delta} g(x))\) as \(x \to \infty\).

def SubpowerBound (f g : ℝ → ℝ) : Prop :=
  ∀ δ : ℝ, 0 < δ → Asymptotics.IsBigO atTop f (fun x ↦ x ^ δ * g x)

Sources

• Polymath8b, arXiv:1407.4897v4, Definition 1.6.

Used by 2

Used byElliott–Halberstam estimate at level \(\theta\) · Generalized Elliott–Halberstam estimate at level \(\theta\)

DefinitionSupport in a dyadic interval#✓fully proved

A finitely supported sequence \(\alpha : \mathbb{N} \to \mathbb{R}\) is supported in the dyadic interval at scale \(N \in \mathbb{R}\) if every \(n\) with \(\alpha(n) \ne 0\) satisfies \(n \ge 1\) and \(N \le n \le 2N\).

def DyadicSupport (α : ℕ →₀ ℝ) (N : ℝ) : Prop :=
  ∀ n ∈ α.support, 1 ≤ n ∧ N ≤ (n : ℝ) ∧ (n : ℝ) ≤ 2 * N

Sources

• Polymath8b v4, Claim 2.6.

Used by 1

Used byGeneralized Elliott–Halberstam estimate at level \(\theta\)

DefinitionDivisor–logarithm bound for a family of sequences#✓fully proved

A family \((\alpha_x)_{x \in \mathbb{R}}\) of finitely supported sequences \(\alpha_x : \mathbb{N} \to \mathbb{R}\) satisfies the divisor–logarithm bound if there are a real number \(C > 0\) and natural numbers \(k\) and \(l\) such that for all sufficiently large real \(x\) and all integers \(n \ge 1\),

\[|\alpha_x(n)| \le C \, \tau(n)^k (\log x)^l,\]

where \(\tau(n)\) is the number of positive divisors of \(n\). The constants \(C\), \(k\) and \(l\) depend neither on \(x\) nor on \(n\).

def DivisorLogBound (α : ℝ → ℕ →₀ ℝ) : Prop :=
  ∃ C : ℝ, ∃ k l : ℕ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
    ∀ n : ℕ, 1 ≤ n → |α x n| ≤
      C * (n.divisors.card : ℝ) ^ k * Real.log x ^ l

Sources

• Polymath8b v4, Claim 2.6.

Used by 1

Used byGeneralized Elliott–Halberstam estimate at level \(\theta\)

DefinitionSiegel–Walfisz hypothesis for a family of sequences#✓fully proved

Let \((\beta_x)_{x \in \mathbb{R}}\) be a family of finitely supported sequences \(\beta_x : \mathbb{N} \to \mathbb{R}\) and let \(M : \mathbb{R} \to \mathbb{R}\). The family satisfies the Siegel–Walfisz hypothesis at scale \(M\) if for every real \(A \ge 1\) there are a real number \(C > 0\) and a natural number \(k\) such that, for all sufficiently large real \(x\) and all natural numbers \(q \ge 1\), \(r \ge 1\) and \(a\) with \(\gcd(a, q) = 1\),

\[|\Delta(\beta_x^{(r)}; a \bmod q)| \le C \, \tau(qr)^k \, M(x) / (\log x)^A.\]

Here \(\beta_x^{(r)}\) is the sequence equal to \(\beta_x(n)\) when \(\gcd(n, r) = 1\) and to \(0\) otherwise, \(\Delta(\cdot\,; a \bmod q)\) is the discrepancy in the residue class of \(a\) modulo \(q\), and \(\tau(m)\) is the number of positive divisors of \(m\).

def SiegelWalfisz (β : ℝ → ℕ →₀ ℝ) (M : ℝ → ℝ) : Prop :=
  ∀ A : ℝ, 1 ≤ A → ∃ C : ℝ, ∃ k : ℕ, 0 < C ∧
    ∀ᶠ x : ℝ in atTop, ∀ q r a : ℕ, (h1q : 1 ≤ q) → 1 ≤ r → Nat.Coprime a q →
      |discrepancy ((β x).filter (fun n ↦ Nat.Coprime n r)) ⟨q, h1q⟩ a| ≤
        C * ((q * r).divisors.card : ℝ) ^ k * M x / Real.log x ^ A

Sources

• Polymath8b v4, Claim 2.6 and its uniformity footnote.

Uses 1 · Used by 1

Statement usesDiscrepancy in a residue class

Used byGeneralized Elliott–Halberstam estimate at level \(\theta\)

DefinitionElliott–Halberstam estimate at level \(\theta\)#✓fully proved

For a real number \(\theta\), the Elliott–Halberstam estimate at level \(\theta\) is the following statement. Let \(Q : \mathbb{R} \to \mathbb{N}\) be such that \(Q(x) = O(x^{\delta} x^{\theta})\) as \(x \to \infty\) for every real \(\delta > 0\), and let \(A \ge 1\) be real. Then there is a real number \(C > 0\) such that for all sufficiently large real \(x\), the averaged discrepancy of \(\Lambda_x\) up to \(Q(x)\) is at most \(C x / (\log x)^A\). Here \(\Lambda_x\) is the sequence equal to the von Mangoldt function \(\Lambda(n)\) for integers \(n \ge 1\) with \(x \le n \le 2x\) and to \(0\) otherwise, and the averaged discrepancy of a sequence \(\alpha\) up to \(Q\) is \(\sum_{q=1}^{Q} \Delta^*(\alpha; q)\), where \(\Delta^*(\alpha; q)\) is the largest absolute value of the discrepancy of \(\alpha\) in a residue class modulo \(q\) coprime to \(q\).

def ElliottHalberstamAt (θ : ℝ) : Prop :=
  ∀ Q : ℝ → ℕ, SubpowerBound (fun x ↦ (Q x : ℝ)) (fun x ↦ x ^ θ) →
    ∀ A : ℝ, 1 ≤ A → ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
      averagedDiscrepancy (dyadicVonMangoldt x) (Q x) ≤ C * x / Real.log x ^ A

Sources

• Polymath8b v4, Claim 2.2.

Uses 3 · Used by 1

Statement usesAveraged discrepancy · Von Mangoldt function on a dyadic interval · Subpower bound

Used byElliott–Halberstam conjecture (dyadic form)

DefinitionGeneralized Elliott–Halberstam estimate at level \(\theta\)#✓fully proved

For a real number \(\theta\), the generalized Elliott–Halberstam estimate at level \(\theta\) is the following statement. Let \(\varepsilon > 0\) be real, let \(N, M : \mathbb{R} \to \mathbb{R}\), and let \((\alpha_x)_{x \in \mathbb{R}}\) and \((\beta_x)_{x \in \mathbb{R}}\) be families of finitely supported sequences \(\mathbb{N} \to \mathbb{R}\). Assume that for all sufficiently large real \(x\) we have \(N(x) > 0\) and \(M(x) > 0\), \(\alpha_x\) is supported in the dyadic interval at scale \(N(x)\) and \(\beta_x\) is supported in the dyadic interval at scale \(M(x)\); that for every real \(\delta > 0\), as \(x \to \infty\), \(x^{\varepsilon} = O(x^{\delta} N(x))\), \(N(x) = O(x^{\delta} x^{1 - \varepsilon})\), \(x^{\varepsilon} = O(x^{\delta} M(x))\) and \(M(x) = O(x^{\delta} x^{1 - \varepsilon})\); that \(N(x) M(x) = O(x)\) and \(x = O(N(x) M(x))\) as \(x \to \infty\); that both families satisfy the divisor–logarithm bound; and that \((\beta_x)\) satisfies the Siegel–Walfisz hypothesis at scale \(M\). Let \(Q : \mathbb{R} \to \mathbb{N}\) be such that \(Q(x) = O(x^{\delta} x^{\theta})\) as \(x \to \infty\) for every real \(\delta > 0\), and let \(A \ge 1\) be real. Then there is a real number \(C > 0\) such that for all sufficiently large real \(x\), the averaged discrepancy of the multiplicative convolution \(\alpha_x \star \beta_x\) up to \(Q(x)\) is at most \(C x / (\log x)^A\).

def GeneralizedElliottHalberstamAt (θ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ N M : ℝ → ℝ, ∀ α β : ℝ → ℕ →₀ ℝ,
    (∀ᶠ x : ℝ in atTop, 0 < N x ∧ 0 < M x ∧
      DyadicSupport (α x) (N x) ∧ DyadicSupport (β x) (M x)) →
    SubpowerBound (fun x ↦ x ^ ε) N →
    SubpowerBound N (fun x ↦ x ^ (1 - ε)) →
    SubpowerBound (fun x ↦ x ^ ε) M →
    SubpowerBound M (fun x ↦ x ^ (1 - ε)) →
    Asymptotics.IsTheta atTop (fun x ↦ N x * M x) (fun x ↦ x) →
    DivisorLogBound α → DivisorLogBound β → SiegelWalfisz β M →
    ∀ Q : ℝ → ℕ, SubpowerBound (fun x ↦ (Q x : ℝ)) (fun x ↦ x ^ θ) →
      ∀ A : ℝ, 1 ≤ A → ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
        averagedDiscrepancy (convolution (α x) (β x)) (Q x) ≤ C * x / Real.log x ^ A

Sources

• Polymath8b v4, Claim 2.6.

Uses 6 · Used by 1

Statement usesAveraged discrepancy · Multiplicative convolution of finitely supported sequences · Divisor–logarithm bound for a family of sequences · Support in a dyadic interval · Siegel–Walfisz hypothesis for a family of sequences · Subpower bound

Used byGeneralized Elliott–Halberstam conjecture (dyadic form)

DefinitionElliott–Halberstam conjecture (dyadic form)#✓fully proved

The Elliott–Halberstam estimate at level \(\theta\) holds for every real number \(\theta\) with \(0 < \theta < 1\).

def ElliottHalberstam : Prop :=
  ∀ θ : ℝ, 0 < θ → θ < 1 → ElliottHalberstamAt θ

Sources

• Polymath8b v4, Theorems 1.1 and 1.3 and Claim 2.2.

Uses 1 · Used by 3

Statement usesElliott–Halberstam estimate at level \(\theta\)

Used byGoldston–Pintz–Yıldırım bound under Elliott–Halberstam · Maynard's bound under Elliott–Halberstam · Prime pairs with \(5\)-smooth difference under Elliott–Halberstam

DefinitionGeneralized Elliott–Halberstam conjecture (dyadic form)#✓fully proved

The generalized Elliott–Halberstam estimate at level \(\theta\) holds for every real number \(\theta\) with \(0 < \theta < 1\).

def GeneralizedElliottHalberstam : Prop :=
  ∀ θ : ℝ, 0 < θ → θ < 1 → GeneralizedElliottHalberstamAt θ

Sources

• Polymath8b v4, Theorem 1.4 and Claim 2.6.

Uses 1 · Used by 1

Statement usesGeneralized Elliott–Halberstam estimate at level \(\theta\)

Used byPolymath8b bound under the generalized Elliott–Halberstam conjecture

TheoremZhang's 2014 bound on prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 70\,000\,000\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted zhang2014UpperBound : primeGapLiminf ≤ (70000000 : WithTop ℕ)

Sources

• Zhang, Annals of Mathematics 179 (2014), 1121-1174; Polymath8b v4, Theorem 1.2.

Uses 1

Statement usesLiminf of prime gaps

TheoremPolymath8a bound 4680 on small prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 4680\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted polymath8a2014UpperBound : primeGapLiminf ≤ (4680 : WithTop ℕ)

Sources

• Polymath, Algebra & Number Theory 8 (2014), 2067-2199; Polymath8b v4, Introduction.

Uses 1

Statement usesLiminf of prime gaps

TheoremMaynard's bound 600 on small prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 600\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

The bound was also obtained independently by Tao.

theorem_wanted maynard2015UpperBound : primeGapLiminf ≤ (600 : WithTop ℕ)

Sources

• Maynard, Annals of Mathematics 181 (2015), 383-413; Polymath8b v4, Theorem 1.3(i).

Uses 1

Statement usesLiminf of prime gaps

TheoremPolymath8b bound 246 on small prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 246\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

The bound is the one stated in the original arXiv version v4; whether the 2015 erratum affects it is unresolved.

theorem_wanted polymath8b2014UpperBound : primeGapLiminf ≤ (246 : WithTop ℕ)

Sources

• Polymath8b, arXiv:1407.4897v4, Theorem 1.4(i), DOI 10.1186/s40687-014-0012-7.

Uses 1

Statement usesLiminf of prime gaps

TheoremZhang's 2026 bound of 240 on prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 240\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted zhang2026UpperBound : primeGapLiminf ≤ (240 : WithTop ℕ)

Sources

• Zhang, Zenodo 10.5281/zenodo.22135842, 28 August 2026, as quoted in constants/88a.md.

Uses 1

Statement usesLiminf of prime gaps

TheoremOpenAI's bound 186 on small prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 186\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted openai2026UpperBound : primeGapLiminf ≤ (186 : WithTop ℕ)

Sources

• OpenAI, Improved short gaps between primes, 30 August 2026, quoted in constants/88a.md.

Uses 1

Statement usesLiminf of prime gaps

TheoremStadlmann's bound 240 on small prime gaps#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. Then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 240\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted stadlmann2026UpperBound : primeGapLiminf ≤ (240 : WithTop ℕ)

Sources

• Stadlmann, arXiv:2608.31126, 31 August 2026, as quoted in constants/88a.md.

Uses 1

Statement usesLiminf of prime gaps

TheoremMaynard's bound under Elliott–Halberstam#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. If the Elliott–Halberstam conjecture holds at every level \(\theta\) with \(0 < \theta < 1\), in Polymath8b's dyadic form, then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 12\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted maynardElliottHalberstamUpperBound :
  Polymath8b.ElliottHalberstam → primeGapLiminf ≤ (12 : WithTop ℕ)

Sources

• Maynard (2015); Polymath8b v4, Theorem 1.3(iii).

Uses 2

Statement usesLiminf of prime gaps · Elliott–Halberstam conjecture (dyadic form)

TheoremGoldston–Pintz–Yıldırım bound under Elliott–Halberstam#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. If the Elliott–Halberstam conjecture holds at every level \(\theta\) with \(0 < \theta < 1\), in Polymath8b's dyadic form, then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 16\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted gpyElliottHalberstamUpperBound :
  Polymath8b.ElliottHalberstam → primeGapLiminf ≤ (16 : WithTop ℕ)

Sources

• Goldston-Pintz-Yıldırım (2009); Polymath8b v4, Theorem 1.1.

Uses 2

Statement usesLiminf of prime gaps · Elliott–Halberstam conjecture (dyadic form)

TheoremPolymath8b bound under the generalized Elliott–Halberstam conjecture#●ready to prove

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. If the generalized Elliott–Halberstam conjecture holds at every level \(\theta\) with \(0 < \theta < 1\), in Polymath8b's dyadic form, then \(\liminf_{n \to \infty} (p_{n+1} - p_n) \le 6\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem_wanted polymath8bGeneralizedElliottHalberstamUpperBound :
  Polymath8b.GeneralizedElliottHalberstam → primeGapLiminf ≤ (6 : WithTop ℕ)

Sources

• Polymath8b v4, Theorem 1.4(xii); the 2015 erratum correction is unavailable.

Uses 2

Statement usesLiminf of prime gaps · Generalized Elliott–Halberstam conjecture (dyadic form)

TheoremTwo primes in infinitely many translates of an admissible 40-tuple#●ready to prove

Let \(h_1, \dots, h_{40}\) be distinct integers forming an admissible tuple: for every prime \(p\), some residue class modulo \(p\) contains none of the \(h_i\). Then there are infinitely many natural numbers \(n\) such that at least two of the integers \(n + h_1, \dots, n + h_{40}\) are prime.

A negative integer or zero is never counted as prime.

theorem_wanted openai2026DHL :
  ∀ h : Fin 40 → ℤ, Function.Injective h →
    MetaMathlibExt.IsHardyLittlewoodAdmissible 40 h →
      Set.Infinite {n : ℕ |
        2 ≤ (Finset.univ.filter (fun i : Fin 40 ↦ Nat.Prime ((n : ℤ) + h i).toNat)).card}

Sources

• OpenAI (2026), Theorem 1.1, as quoted in the 186 row of constants/88a.md.

Uses 1

Statement usesHardy–Littlewood admissible tuples

DefinitionThe forty shifts behind the bound 186#✓fully proved

The list of the forty integers \(0, 2, 6, 12, 20, 26, 30, 32, 36, 42, 48, 50, 56, 60, 68, 72, 78, 86, 90, 92, 98, 102, 110, 116, 120, 126, 132, 138, 140, 146, 152, 156, 158, 162, 168, 170, 176, 180, 182, 186\), in this order.

def shifts186 : List ℤ :=
  [0, 2, 6, 12, 20, 26, 30, 32, 36, 42, 48, 50, 56, 60, 68, 72, 78, 86, 90, 92,
    98, 102, 110, 116, 120, 126, 132, 138, 140, 146, 152, 156, 158, 162,
    168, 170, 176, 180, 182, 186]

Sources

• OpenAI (2026), equation (1.3).

Used by 1

Used byThe explicit 40-tuple for the gap bound 186

DefinitionThe explicit 40-tuple for the gap bound 186#✓fully proved

The \(40\)-tuple of integers \(h = (h_0, \dots, h_{39})\) whose entries, in order, are \(0, 2, 6, 12, 20, 26, 30, 32, 36, 42, 48, 50, 56, 60, 68, 72, 78, 86, 90, 92, 98, 102, 110, 116, 120, 126, 132, 138, 140, 146, 152, 156, 158, 162, 168, 170, 176, 180, 182, 186\).

def tuple186 (i : Fin 40) : ℤ := shifts186.get ⟨i.val, by simp [shifts186]⟩

Sources

• OpenAI (2026), equation (1.3), and the 186 row of constants/88a.md.

Uses 1 · Used by 4

Statement usesThe forty shifts behind the bound 186

Used byThe explicit 40-tuple is admissible · The entries of the explicit 40-tuple lie between 0 and 186 · The explicit 40-tuple has diameter 186 · The explicit 40-tuple has distinct entries

TheoremThe explicit 40-tuple has distinct entries#✓fully proved

Let \(h = (h_0, \dots, h_{39})\) be the explicit \(40\)-tuple of integers \((0, 2, 6, \dots, 182, 186)\). Then the entries of \(h\) are pairwise distinct: \(h_i = h_j\) implies \(i = j\).

theorem tuple186_injective : Function.Injective tuple186

Sources

• the explicit tuple in OpenAI (2026), equation (1.3).

Uses 1

Statement usesThe explicit 40-tuple for the gap bound 186

TheoremThe entries of the explicit 40-tuple lie between 0 and 186#✓fully proved

Let \(h = (h_0, \dots, h_{39})\) be the explicit \(40\)-tuple of integers \((0, 2, 6, \dots, 182, 186)\). Then \(0 \le h_i \le 186\) for every \(i \in \{0, \dots, 39\}\).

theorem tuple186_bounds : ∀ i : Fin 40, 0 ≤ tuple186 i ∧ tuple186 i ≤ 186

Sources

• the explicit tuple in OpenAI (2026), equation (1.3).

Uses 1 · Used by 1

Statement usesThe explicit 40-tuple for the gap bound 186

Used byThe explicit 40-tuple has diameter 186

TheoremThe explicit 40-tuple has diameter 186#✓fully proved

Let \(h = (h_0, \dots, h_{39})\) be the explicit \(40\)-tuple of integers \((0, 2, 6, \dots, 182, 186)\). The largest value in the set \(\{h_0, \dots, h_{39}\}\) minus the smallest value in it equals \(186\).

theorem tuple186_diameter :
    (Finset.univ.image tuple186).max' (by simp) -
      (Finset.univ.image tuple186).min' (by simp) = 186

Sources

• OpenAI (2026), equation (1.3), as quoted in constants/88a.md.

Uses 2

Statement usesThe explicit 40-tuple for the gap bound 186

Proof usesThe entries of the explicit 40-tuple lie between 0 and 186

TheoremThe explicit 40-tuple is admissible#✓fully proved

Let \(h = (h_0, \dots, h_{39})\) be the explicit \(40\)-tuple of integers \((0, 2, 6, \dots, 182, 186)\). Then \(h\) is Hardy–Littlewood admissible: for every prime \(p\), the number of residue classes modulo \(p\) that contain an entry of \(h\) is not \(p\).

theorem tuple186_admissible : MetaMathlibExt.IsHardyLittlewoodAdmissible 40 tuple186

Sources

• OpenAI (2026), equation (1.3).

Uses 3

Statement usesHardy–Littlewood admissible tuples · The explicit 40-tuple for the gap bound 186

Proof usesNumber of residue classes met by an integer tuple

14 fully proved11 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.