Conjectures.io

Number theory

Erdős 853 - part ii

Let dn=pn+1−pnd_n = p_{n+1} - p_n, where pnp_n is the nnth prime. Let r(x)r(x) be the smallest even integer tt such that dn=td_n = t has no solutions for n≤xn \le x. Is it true that r(x)/log⁡x→∞r(x) / \log x \to \infty?

References

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«853»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos853.erdos_853.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/853.lean

Source type SHA-256
sha256:35cc28a6d3947513cdcb0d0cfa66afc02eae6c01da68156231c9c953f980b5b9
Task id
fc-379fc029-parts-ii-2b0774c1ab-formalized-v1
Task commitment
sha256:b38bef1b958be126a6c102f82670484f6900ab7865ea35d29d8fe60bad98f142

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.