Erdős Problem 1138

References:

• erdosproblems.com/1138
• [Va99] Vardi, I., Prime census. (1999).
• [Kum26] Kumrawat, S., Disproof of Erdős Problem 1138.

Note that the conjecture has a claimed disproof found at: https://sourish-kumrawat.github.io/papers/Erdos_1138.pdf, see the discussion section on the Erdos problems website for more information.

noncomputable def Erdos1138.sup_primeGap (x : ℝ) : ℕ

The maximal prime gap below $x$, i.e. $d(x) = \max_{p_n < x}(p_{n+1} - p_n)$, where $p_n$ denotes the $n$-th prime.

Equations

• Erdos1138.sup_primeGap x = (Finset.range ⌈x⌉₊.primeCounting').sup primeGap

@[reducible, inline]

abbrev Erdos1138.snd_gt_half_fst : Filter (ℝ × ℝ)

The filter on $\mathbb{R} \times \mathbb{R}$ corresponding to sending $x \to \infty$ subject to $x/2 < y < x$

Equations

• Erdos1138.snd_gt_half_fst = Filter.comap Prod.fst Filter.atTop ⊓ Filter.principal {p : ℝ × ℝ | p.2 ∈ Set.Ioo (p.1 / 2) p.1}

noncomputable def Erdos1138.primeCount_Ioc_mul_const (C : ℝ) : ℝ × ℝ → ℝ

Given a pair $(x,y)$, this is the amount of primes in the interval above $y$, of length equalling the largest prime gap before $x$, scaled by a constant $C$.

Equations

• Erdos1138.primeCount_Ioc_mul_const C (x_1, y) = ↑⌊y + C * ↑(Erdos1138.sup_primeGap x_1)⌋₊.primeCounting - ↑⌊y⌋₊.primeCounting

theorem Erdos1138.erdos_1138 : False ↔ ∀ C > 1, Asymptotics.IsEquivalent snd_gt_half_fst (primeCount_Ioc_mul_const C) fun (x : ℝ × ℝ) => match x with | (x, y) => C * ↑(sup_primeGap x) / Real.log y

Erdős Problem 1138. Let $x/2 < y < x$ and $C > 1$. If $d = \max_{p_n < x}(p_{n+1} - p_n)$, where $p_n$ denotes the $n$-th prime, then is it true that $$\pi(y + Cd) - \pi(y) \sim \frac{Cd}{\log y}$$?