Erdős problem 1138

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}$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1138.lean

Retained formal statement1 of 1

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}$ ?

FormalConjectures/ErdosProblems/1138.leanErdos1138.erdos_11385 linesExact file

1False ↔2  ∀ C > 1,3    Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x =>4      match x with5      | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.