Hardy–Littlewood prime tuples conjecture

DefinitionNumber of residue classes met by an integer tuple#✓fully proved

For an \(m\)-tuple \(b = (b_1, \dots, b_m)\) of integers and a natural number \(p\), \(v_p(b)\) is the number of distinct values among the remainders \(b_1 \bmod p, \dots, b_m \bmod p\), that is, the number of residue classes modulo \(p\) that contain an entry of \(b\).

def hardyLittlewoodResidueCount (m : ℕ) (b : Fin m → ℤ) (p : ℕ) : ℕ :=
  (Finset.univ.image (fun i => (b i) % (p : ℤ))).card

Used by 5

Used byThe explicit 40-tuple is admissible · Euler factors of the Hardy–Littlewood singular series · Missing a residue class modulo a prime · Hardy–Littlewood admissible tuples · Hardy–Littlewood admissibility via the set of entries

DefinitionHardy–Littlewood admissible tuples#✓fully proved

An \(m\)-tuple \(b\) of integers is admissible when \(v_p(b) \ne p\) for every prime \(p\), where \(v_p(b)\) is the number of residue classes modulo \(p\) that contain an entry of \(b\).

def IsHardyLittlewoodAdmissible (m : ℕ) (b : Fin m → ℤ) : Prop :=
  ∀ p : ℕ, Nat.Prime p → hardyLittlewoodResidueCount m b p ≠ p

Uses 1 · Used by 4

Statement usesNumber of residue classes met by an integer tuple

Used byTwo primes in infinitely many translates of an admissible 40-tuple · The explicit 40-tuple is admissible · Hardy–Littlewood prime-tuple conjecture · Hardy–Littlewood admissibility via the set of entries

DefinitionThe prime-tuple counting function#✓fully proved

For an \(m\)-tuple \(b = (b_1, \dots, b_m)\) of integers and a natural number \(x\), \(P(x; b)\) is the number of integers \(n\) with \(1 \le n \le x\) such that each of \(n + b_1, \dots, n + b_m\) is a (positive) prime number.

noncomputable def hardyLittlewoodPrimeTupleCount (m : ℕ) (b : Fin m → ℤ) (x : ℕ) : ℕ :=
  Set.ncard { n : ℕ | 1 ≤ n ∧ n ≤ x ∧ ∀ i, ∃ q : ℕ, Nat.Prime q ∧ (n : ℤ) + b i = (q : ℤ) }

Used by 1

Used byHardy–Littlewood prime-tuple conjecture

DefinitionEuler factors of the Hardy–Littlewood singular series#✓fully proved

For an \(m\)-tuple \(b\) of integers and a natural number \(p\), the Euler factor of \(b\) at \(p\) is the real number

\[\left(\frac{p}{p-1}\right)^{m-1} \frac{p - v_p(b)}{p - 1},\]

where \(v_p(b)\) is the number of residue classes modulo \(p\) that contain an entry of \(b\), the exponent \(m - 1\) is truncated at \(0\) (so it is \(0\) when \(m = 0\)), and division by \(0\) gives \(0\).

noncomputable def hardyLittlewoodEulerFactor (m : ℕ) (b : Fin m → ℤ) (p : ℕ) : ℝ :=
  ((p : ℝ) / ((p : ℝ) - 1)) ^ (m - 1) *
    (((p : ℝ) - (hardyLittlewoodResidueCount m b p : ℝ)) / ((p : ℝ) - 1))

Uses 1 · Used by 1

Statement usesNumber of residue classes met by an integer tuple

Used byThe Hardy–Littlewood singular series

DefinitionThe Hardy–Littlewood singular series#✓fully proved

For an \(m\)-tuple \(b\) of integers, the singular series \(\mathfrak{S}(b)\) is the product over all primes \(p\) of the Euler factors

\[\left(\frac{p}{p-1}\right)^{m-1} \frac{p - v_p(b)}{p - 1},\]

where \(v_p(b)\) is the number of residue classes modulo \(p\) that contain an entry of \(b\) and the exponent \(m - 1\) is truncated at \(0\). The product is the limit in \(\mathbb{R}\) of the products over finite sets \(S\) of primes, with the sets \(S\) directed by inclusion; this limit may be \(0\) (for instance when some Euler factor is \(0\)), and \(\mathfrak{S}(b)\) is \(1\) when the limit does not exist.

noncomputable def hardyLittlewoodSingularSeries (m : ℕ) (b : Fin m → ℤ) : ℝ :=
  ∏' (p : ℕ), (if Nat.Prime p then hardyLittlewoodEulerFactor m b p else 1)

Uses 1 · Used by 1

Statement usesEuler factors of the Hardy–Littlewood singular series

Used byHardy–Littlewood prime-tuple conjecture

DefinitionAdmissible finite sets of integers#✓fully proved

A finite set \(H\) of integers is admissible if for every prime \(p\) there is a residue class \(r\) modulo \(p\) that contains no element of \(H\).

A tuple of integers is called Hardy–Littlewood admissible when, for every prime \(p\), its entries meet fewer than \(p\) residue classes modulo \(p\); this holds exactly when its set of entries is admissible.

def IsAdmissibleFinset (H : Finset ℤ) : Prop :=
  ∀ p : ℕ, p.Prime → ∃ r : ZMod p, ∀ h ∈ H, (h : ZMod p) ≠ r

Sources

• Carol Wu, On Smooth Gaps between Primes Using the Maynard-Tao Sieve, INTEGERS 25 (2025), Article A44, Definition 1.

Used by 7

Used byAdmissible difference-smooth sets of every size · Prime \(m\)-tuples with smooth gaps · Maynard–Tao theorem · Admissible sets are not difference smooth at small bounds · The empty set is admissible · The set \(\{0\}\) is admissible · Hardy–Littlewood admissibility via the set of entries

TheoremMissing a residue class modulo a prime#✓fully proved

Let \(b = (b_1, \dots, b_m)\) be an \(m\)-tuple of integers, let \(p\) be a prime, and let \(v_p(b)\) be the number of residue classes modulo \(p\) that contain an entry of \(b\). Then \(v_p(b) \ne p\) if and only if there is a residue class \(r\) modulo \(p\) with \(b_i \not\equiv r \pmod p\) for every \(i\).

theorem hardyLittlewoodResidueCount_ne_iff (m : ℕ) (b : Fin m → ℤ) {p : ℕ} (hp : p.Prime) :
    hardyLittlewoodResidueCount m b p ≠ p ↔
      ∃ r : ZMod p, ∀ i, (b i : ZMod p) ≠ r

Sources

• Carol Wu, On Smooth Gaps between Primes Using the Maynard-Tao Sieve, INTEGERS 25 (2025), Article A44, Definition 1.

Uses 1 · Used by 1

Statement usesNumber of residue classes met by an integer tuple

Used byHardy–Littlewood admissibility via the set of entries

TheoremHardy–Littlewood admissibility via the set of entries#✓fully proved

A tuple of integers is Hardy–Littlewood admissible exactly when its set of entries is admissible.

theorem isHardyLittlewoodAdmissible_iff_isAdmissibleFinset (m : ℕ) (b : Fin m → ℤ) :
    IsHardyLittlewoodAdmissible m b ↔ IsAdmissibleFinset (Finset.univ.image b)

Sources

• Carol Wu, On Smooth Gaps between Primes Using the Maynard-Tao Sieve, INTEGERS 25 (2025), Article A44, Definition 1.

Uses 4

Statement usesAdmissible finite sets of integers · Hardy–Littlewood admissible tuples

Proof usesNumber of residue classes met by an integer tuple · Missing a residue class modulo a prime

TheoremThe empty set is admissible#✓fully proved

The empty set of integers is admissible: for every prime \(p\), some residue class modulo \(p\) contains none of its elements.

theorem isAdmissibleFinset_empty : IsAdmissibleFinset ∅

Sources

• Carol Wu, On Smooth Gaps between Primes Using the Maynard-Tao Sieve, INTEGERS 25 (2025), Article A44, Definition 1.

Uses 1

Statement usesAdmissible finite sets of integers

TheoremThe set \(\{0\}\) is admissible#✓fully proved

The one-element set \(\{0\}\) of integers is admissible: for every prime \(p\) it misses the residue class of \(1\) modulo \(p\).

theorem isAdmissibleFinset_singleton_zero : IsAdmissibleFinset {0}

Sources

• Carol Wu, On Smooth Gaps between Primes Using the Maynard-Tao Sieve, INTEGERS 25 (2025), Article A44, Definition 1.

Uses 1

Statement usesAdmissible finite sets of integers

TheoremHardy–Littlewood prime-tuple conjecture#●ready to prove

Let \(m \ge 1\) and let \(b = (b_1, \dots, b_m)\) be an admissible \(m\)-tuple of pairwise distinct integers. Then the singular series \(\mathfrak{S}(b)\) is nonzero, and the prime-tuple count \(P(x; b)\), the number of integers \(n\) with \(1 \le n \le x\) such that \(n + b_1, \dots, n + b_m\) are all prime, satisfies

\[P(x; b) \sim \mathfrak{S}(b) \int_2^x \frac{du}{(\log u)^m}\]

as the natural number \(x\) tends to infinity.

theorem_wanted hardyLittlewoodPrimeTupleConjecture
    (m : ℕ) (hm : 0 < m) (b : Fin m → ℤ) (hb : Function.Injective b)
    (hadmissible : IsHardyLittlewoodAdmissible m b) :
    hardyLittlewoodSingularSeries m b ≠ 0 ∧
      Asymptotics.IsEquivalent Filter.atTop
        (fun x : ℕ => (hardyLittlewoodPrimeTupleCount m b x : ℝ))
        (fun x : ℕ => hardyLittlewoodSingularSeries m b *
          ∫ u in (2 : ℝ)..(x : ℝ), 1 / (Real.log u) ^ m)

Sources

• Hùng Việt Chu, Nathan McNew, Steven J. Miller, Victor Xu, and Sean Zhang, When Sets Can and Cannot Have Sum-Dominant Subsets, https://cs.uwaterloo.ca/journals/JIS/VOL21/Miller/miller8.tex.

Uses 3

Statement usesHardy–Littlewood admissible tuples · The prime-tuple counting function · The Hardy–Littlewood singular series

10 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.