Prime gaps

DefinitionConsecutive primes#✓fully proved

Natural numbers \(p\) and \(q\) are consecutive primes when \(p\) and \(q\) are prime, \(p < q\), and every prime \(r\) satisfies \(r \le p\) or \(q \le r\); that is, no prime lies strictly between \(p\) and \(q\).

This is the usual meaning of successive primes \(p_k, p_{k+1}\) used in the source papers.

def AreConsecutivePrimes (p q : ℕ) : Prop :=
  Nat.Prime p ∧ Nat.Prime q ∧ p < q ∧ ∀ r, Nat.Prime r → r ≤ p ∨ q ≤ r
Sources
Used by 3
Used bySuccessive primes in the enumeration are consecutive · Block of consecutive primes · Primes just above a primorial, for a consecutive-prime pair

DefinitionBlock of consecutive primes#✓fully proved

A list \(l\) of natural numbers is a block of consecutive primes when \(l\) is nonempty, every entry of \(l\) is prime, \(l\) is strictly increasing, and every two adjacent entries of \(l\) are consecutive primes.

def IsConsecutivePrimeBlock (l : List ℕ) : Prop :=
  l ≠ [] ∧ (∀ p ∈ l, Nat.Prime p) ∧ List.Pairwise (· < ·) l ∧
    ∀ x ∈ l.consecutivePairs, AreConsecutivePrimes x.1 x.2
Sources
  • see the sources cited on AreConsecutivePrimes for occurrences of blocks pₖ, pₖ₊₁, …, pₘ of consecutive primes.
Uses 1 · Used by 1
Statement usesConsecutive primes
Used byRestricted block of consecutive primes

DefinitionRestricted block of consecutive primes#✓fully proved

Let \(P\) be a predicate on natural numbers. A list \(l\) of natural numbers is a block of consecutive primes restricted by \(P\) when \(l\) is a block of consecutive primes and every entry of \(l\) satisfies \(P\).

This covers, for example, the factorial- and primorial-bounded blocks in the source papers by choosing the corresponding predicate \(P\).

def IsRestrictedConsecutivePrimeBlock (P : ℕ → Prop) (l : List ℕ) : Prop :=
  IsConsecutivePrimeBlock l ∧ ∀ p ∈ l, P p
Uses 1
Statement usesBlock of consecutive primes

DefinitionPrime gap#✓fully proved

Let \(p_0 = 2\), \(p_1 = 3\), \(p_2 = 5, \dots\) be the primes in increasing order, indexed from \(0\). For a natural number \(n\), the prime gap at \(n\) is \(p_{n+1} - p_n\).

noncomputable def primeGap (n : ℕ) : ℕ := (n + 1).nth Nat.Prime - n.nth Nat.Prime
Used by 10
Used byErdős Problem 6 (increasing prime gaps) · A prime gap equals two exactly at a twin prime · Liminf of prime gaps · The liminf of prime gaps is two exactly when there are infinitely many twin primes · When the liminf of prime gaps is at most a given bound · Finite liminf of prime gaps and bounded gaps between primes · Prime gaps are positive · Largest prime gap below \(x\) · Prime gaps after the first are at least two · The liminf of prime gaps is at least two

DefinitionLiminf of prime gaps#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. The liminf of prime gaps is \(\liminf_{n \to \infty} g_n\), taken in \(\mathbb{N} \cup \{\infty\}\); the value \(\infty\) is allowed.

noncomputable def primeGapLiminf : WithTop ℕ :=
  Filter.liminf (fun n : ℕ ↦ (primeGap n : WithTop ℕ)) Filter.atTop
Uses 1 · Used by 14
Statement usesPrime gap
Used byGoldston–Pintz–Yıldırım bound under Elliott–Halberstam · Maynard's bound under Elliott–Halberstam · Maynard's bound 600 on small prime gaps · OpenAI's bound 186 on small prime gaps · Polymath8a bound 4680 on small prime gaps · Polymath8b bound under the generalized Elliott–Halberstam conjecture · Polymath8b bound 246 on small prime gaps · Stadlmann's bound 240 on small prime gaps · Zhang's 2014 bound on prime gaps · Zhang's 2026 bound of 240 on prime gaps · The liminf of prime gaps is two exactly when there are infinitely many twin primes · When the liminf of prime gaps is at most a given bound · Finite liminf of prime gaps and bounded gaps between primes · The liminf of prime gaps is at least two

TheoremSuccessive primes in the enumeration are consecutive#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order. For every \(n \in \mathbb{N}\), \(p_n\) and \(p_{n+1}\) are consecutive primes: both are prime, \(p_n < p_{n+1}\), and no prime lies strictly between them.

theorem consecutive_nth_prime (n : ℕ) :
    MetaMathlibExt.AreConsecutivePrimes (Nat.nth Nat.Prime n) (Nat.nth Nat.Prime (n + 1))
Uses 1
Statement usesConsecutive primes

TheoremPrime gaps are positive#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. Then \(g_n > 0\) for every \(n \in \mathbb{N}\), including \(n = 0\).

theorem primeGap_pos (n : ℕ) : 0 < primeGap n
Uses 1 · Used by 1
Statement usesPrime gap
Used byPrime gaps after the first are at least two

TheoremPrime gaps after the first are at least two#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. For every \(n \ge 1\), \(g_n \ge 2\).

theorem two_le_primeGap (n : ℕ) (hn : 1 ≤ n) : 2 ≤ primeGap n
Uses 2 · Used by 3
Statement usesPrime gap
Proof usesPrime gaps are positive
Used byA prime gap equals two exactly at a twin prime · The liminf of prime gaps is two exactly when there are infinitely many twin primes · The liminf of prime gaps is at least two

TheoremThe liminf of prime gaps is at least two#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. Then \(\liminf_{n \to \infty} g_n \ge 2\), where the liminf is taken in \(\mathbb{N} \cup \{\infty\}\).

theorem two_le_primeGapLiminf : 2 ≤ primeGapLiminf
Uses 3 · Used by 1
Statement usesLiminf of prime gaps
Proof usesPrime gaps after the first are at least two · Prime gap
Used byThe liminf of prime gaps is two exactly when there are infinitely many twin primes

TheoremWhen the liminf of prime gaps is at most a given bound#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order, let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap, and let \(L = \liminf_{n \to \infty} g_n\), taken in \(\mathbb{N} \cup \{\infty\}\). For every natural number \(B\), \(L \le B\) if and only if \(g_n \le B\) for infinitely many \(n\).

theorem primeGapLiminf_le_iff_infinite (B : ℕ) :
    primeGapLiminf ≤ (B : WithTop ℕ) ↔ Set.Infinite {n : ℕ | primeGap n ≤ B}
Uses 2 · Used by 2
Statement usesLiminf of prime gaps · Prime gap
Used byThe liminf of prime gaps is two exactly when there are infinitely many twin primes · Finite liminf of prime gaps and bounded gaps between primes

TheoremFinite liminf of prime gaps and bounded gaps between primes#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order, let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap, and let \(L = \liminf_{n \to \infty} g_n\), taken in \(\mathbb{N} \cup \{\infty\}\). Then \(L \ne \infty\) if and only if there is a natural number \(B > 0\) such that infinitely many primes \(p\) admit a prime \(q\) with \(p < q\) and \(q - p \le B\).

theorem primeGapLiminf_ne_top_iff_bounded_pairs :
    primeGapLiminf ≠ ⊤ ↔ ∃ B : ℕ, 0 < B ∧
      Set.Infinite {p : ℕ | Nat.Prime p ∧
        ∃ q : ℕ, Nat.Prime q ∧ p < q ∧ q - p ≤ B}
Uses 3
Statement usesLiminf of prime gaps
Proof usesWhen the liminf of prime gaps is at most a given bound · Prime gap

TheoremA prime gap equals two exactly at a twin prime#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. For every \(n \in \mathbb{N}\), \(g_n = 2\) if and only if \(p_n + 2\) is prime.

theorem primeGap_eq_two_iff (n : ℕ) :
    primeGap n = 2 ↔ Nat.Prime (Nat.nth Nat.Prime n + 2)
Uses 2 · Used by 1
Statement usesPrime gap
Proof usesPrime gaps after the first are at least two
Used byThe liminf of prime gaps is two exactly when there are infinitely many twin primes

TheoremThe liminf of prime gaps is two exactly when there are infinitely many twin primes#✓fully proved

Let \(p_0 < p_1 < p_2 < \cdots\) be the primes in increasing order and let \(g_n = p_{n+1} - p_n\) be the \(n\)-th prime gap. Then \(\liminf_{n \to \infty} g_n = 2\), taken in \(\mathbb{N} \cup \{\infty\}\), if and only if there are infinitely many primes \(p\) such that \(p + 2\) is also prime.

theorem primeGapLiminf_eq_two_iff :
    primeGapLiminf = 2 ↔ Set.Infinite {p : ℕ | Nat.Prime p ∧ Nat.Prime (p + 2)}
Uses 6
Statement usesLiminf of prime gaps
Proof usesWhen the liminf of prime gaps is at most a given bound · A prime gap equals two exactly at a twin prime · Prime gaps after the first are at least two · The liminf of prime gaps is at least two · Prime gap

DefinitionLargest prime gap below \(x\)#✓fully proved

Let \(p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots\) be the primes in increasing order. For a real number \(x\), \(d(x)\) is the largest prime gap \(p_{n+1} - p_n\) over all \(n\) with \(p_n < x\) (the next prime \(p_{n+1}\) may exceed \(x\)), and \(d(x) = 0\) when no prime is less than \(x\).

noncomputable def supPrimeGap (x : ℝ) : ℕ :=
  (Finset.range (Nat.primeCounting' ⌈x⌉₊)).sup primeGap
Uses 1 · Used by 2
Statement usesPrime gap
Used byPrimes in a window of \(C\) maximal prime gaps · Vardi's prime-gap asymptotic

AbbreviationThe regime \(x \to \infty\) with \(x/2 < y < x\)#✓fully proved

The filter on pairs \((x, y)\) of real numbers along which \(x \to \infty\) while \(x/2 < y < x\): a set of pairs belongs to it exactly when it contains every pair \((x, y)\) with \(x/2 < y < x\) and \(x\) sufficiently large.

abbrev sndGtHalfFst : Filter (ℝ × ℝ) :=
  atTop.comap Prod.fst ⊓ Filter.principal {p | p.2 ∈ Set.Ioo (p.1 / 2) p.1}
Used by 1
Used byVardi's prime-gap asymptotic

DefinitionPrimes in a window of \(C\) maximal prime gaps#✓fully proved

Let \(p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots\) be the primes in increasing order, let \(\pi\) be the prime-counting function, and for real \(x\) let \(d(x)\) be the largest prime gap \(p_{n+1} - p_n\) over all \(n\) with \(p_n < x\), with \(d(x) = 0\) when no prime is less than \(x\). For a real number \(C\), this is the function on pairs \((x, y)\) of real numbers given by \(\pi(\lfloor y + C\,d(x) \rfloor) - \pi(\lfloor y \rfloor)\), where the floors are taken in \(\mathbb{N}\) (so negative numbers have floor \(0\)) and the difference is taken in \(\mathbb{R}\).

When \(C \ge 0\) this is the number of primes in the interval \((y, y + C\,d(x)]\).

noncomputable def primeCountIocMulConst (C : ℝ) : (ℝ × ℝ) → ℝ :=
  fun (x, y) ↦ (Nat.primeCounting ⌊y + C * supPrimeGap x⌋₊ - Nat.primeCounting ⌊y⌋₊)
Uses 1 · Used by 1
Statement usesLargest prime gap below \(x\)
Used byVardi's prime-gap asymptotic

DefinitionVardi's prime-gap asymptotic#✓fully proved

Let \(\pi\) be the prime-counting function and, for real \(x\), let \(d(x)\) be the largest prime gap \(p_{n+1} - p_n\) over the primes \(p_n < x\). The proposition states that for every real \(C > 1\),

\[ \pi(\lfloor y + C\,d(x) \rfloor) - \pi(\lfloor y \rfloor) \sim \frac{C\,d(x)}{\log y} \]

as \(x \to \infty\) over pairs \((x, y)\) of reals with \(x/2 < y < x\), where \(\sim\) means that the difference of the two sides is \(o\) of the right-hand side.

This proposition is false (Erdős Problem 1138 was resolved in the negative).

def vardiAsymptotic : Prop :=
  ∀ C > 1,
    primeCountIocMulConst C ~[sndGtHalfFst] fun (x, y) ↦
      C * (supPrimeGap x) / Real.log y
Uses 3 · Used by 2
Statement usesPrimes in a window of \(C\) maximal prime gaps · The regime \(x \to \infty\) with \(x/2 < y < x\) · Largest prime gap below \(x\)
Used byNegation of Vardi's prime-gap asymptotic · Vardi's prime-gap asymptotic is false

DefinitionNegation of Vardi's prime-gap asymptotic#✓fully proved

The proposition that Vardi's prime-gap asymptotic does not hold.

def disprovedVardi : Prop := ¬ vardiAsymptotic
Uses 1
Statement usesVardi's prime-gap asymptotic

TheoremVardi's prime-gap asymptotic is false#●ready to prove

Let \(\pi\) be the prime-counting function and, for real \(x\), let \(d(x)\) be the largest prime gap \(p_{n+1} - p_n\) over the primes \(p_n < x\). It is not true that for every real \(C > 1\), \(\pi(\lfloor y + C\,d(x) \rfloor) - \pi(\lfloor y \rfloor)\) is asymptotically equivalent to \(C\,d(x) / \log y\) as \(x \to \infty\) over pairs \((x, y)\) with \(x/2 < y < x\).

This resolves Erdős Problem 1138 in the negative (Sunder, Kumrawat and Cheri, with GPT 5.5; the disproof is Lean-verified).

public theorem_wanted vardiAsymptotic_refuted : ¬ vardiAsymptotic
Sources
  • Sunder, Kumrawat, Cheri, and GPT 5.5 (Lean-verified disproof), per erdosproblems.com/1138, https://www.erdosproblems.com/1138; Hrishi Sunder, Sourish Kumrawat, and Kireet Cheri, An Elementary Obstruction to a Uniform Prime-Gap Asymptotic (2026), https://github.com/sourish-kumrawat/sourish-kumrawat.github.io/blob/adcbf7ea4e6f57b84001c372a7f8093c95fe7b10/papers/Erdos_1138.pdf; Lean disproof of Erdos Problem 1138, YanYablonovskiy/formal-conjectures, https://github.com/YanYablonovskiy/formal-conjectures/blob/7c134317104d3b98ecc751afbb79ec0adddf8e7c/FormalConjectures/ErdosProblems/1138a.lean#L497.
Uses 1
Statement usesVardi's prime-gap asymptotic

TheoremErdős Problem 6 (increasing prime gaps)#●ready to prove

Let \(p_0 = 2\), \(p_1 = 3\), \(p_2 = 5, \dots\) be the primes in increasing order and let \(d_n = p_{n+1} - p_n\) be the prime gap at \(n\). There are infinitely many natural numbers \(n\) with \(d_n < d_{n+1} < d_{n+2}\).

This was proved by Banks, Freiberg and Turnage-Butterbaugh using the Maynard–Tao machinery.

public theorem_wanted conjecture_holds : conjecture
Sources
  • William D. Banks, Tristan Freiberg, and Caroline L. Turnage-Butterbaugh, Consecutive primes in tuples, Acta Arith. 167 (2015), 261-266; arXiv:1311.7003, https://arxiv.org/abs/1311.7003.
Uses 1
Statement usesPrime gap
18 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.