Erdős problem 853 · problems.science

Let $d_n = p_{n+1} - p_n$ , where $p_n$ is the $n$ th prime. Let $r(x)$ be the smallest even integer $t$ such that $d_n = t$ has no solutions for $n \le x$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

853.lean

Retained formal statement2 of 2

Let $d_n = p_{n+1} - p_n$ , where $p_n$ is the $n$ th prime. Let $r(x)$ be the smallest even integer $t$ such that $d_n = t$ has no solutions for $n \le x$ .

Is it true that $r(x) / \log x \to \infty$ ?

FormalConjectures/ErdosProblems/853.leanErdos853.erdos_853.parts.ii1 lineExact file

1Filter.Tendsto (fun n => ↑(Erdos853.r n) / Real.log ↑n) Filter.atTop Filter.atTop

OpenStatement only, no proof

Sources

Search problems.science