Erdős Problem 17

Reference: erdosproblems.com/17

def Erdos17.IsClusterPrime (p : ℕ) : Prop

A prime $p$ is a cluster prime if every even natural number $n \le p - 3$ can be written as a difference of two primes $q_1 - q_2$ with $q_1, q_2 \le p$.

Equations

• Erdos17.IsClusterPrime p = (Nat.Prime p ∧ ∀ {n : ℕ}, Even n → ↑n ≤ ↑p - 3 → ∃ (q₁ : ℕ) (q₂ : ℕ), Nat.Prime q₁ ∧ Nat.Prime q₂ ∧ q₁ ≤ p ∧ q₂ ≤ p ∧ ↑n = ↑q₁ - ↑q₂)

theorem Erdos17.erdos_17 : {p : ℕ | IsClusterPrime p}.Infinite ↔ sorry

Erdős Problem 17. Are there infinitely many cluster primes?

noncomputable def Erdos17.clusterPrimeCount (n : ℕ) : ℕ

The counting function of cluster primes $\le n$.

Equations

• Erdos17.clusterPrimeCount n = Nat.card ↑{p : ℕ | p ≤ n ∧ Erdos17.IsClusterPrime p}

theorem Erdos17.erdos_17.variants.upper_BES {A : ℝ} (hA : 0 < A) : (fun (x : ℕ) => ↑(clusterPrimeCount x)) =O[Filter.atTop] fun (x : ℕ) => ↑x / Real.log ↑x ^ A

In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound $$\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}$$ for every real $A > 0$.

[BES99] Blecksmith, Richard and Erd\H os, Paul and Selfridge, J. L., Cluster primes. Amer. Math. Monthly (1999), 43--48.

theorem Erdos17.erdos_17.variants.upper_Elsholtz : ∃ (C : ℝ), 0 < C ∧ ∀ c ∈ Set.Ioo 0 (1 / 8), Asymptotics.IsBigOWith C Filter.atTop (fun (x : ℕ) => ↑(clusterPrimeCount x)) fun (x : ℕ) => ↑x * Real.exp (-c * Real.log (Real.log ↑x) ^ 2)

In 2003, Elsholtz [El03] refined the upper bound to $$\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)$$ for every real $0 < c < 1/8$.

[El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.

theorem Erdos17.isClusterPrime_97_isLeast_non_cluster : IsLeast {p : ℕ | Nat.Prime p ∧ ¬IsClusterPrime p} 97

$97$ is the smallest prime that is not a cluster prime.