Erdős Problem #852

The question

erdos_852.parts.i. Let $d_n=p_{n+1}-p_n$, where $p_n$ is the $n$th prime. Let $h(x)$ be maximal such that for some $n<x$ the numbers $d_n,d_{n+1},\dots ,d_{n+h(x)-1}$ are all distinct [Er85c]. Estimate $h(x)$. In particular, is it true that $$h(x)>(\log x{)}^c$$ for some constant $c>0$?

The statement avoids defining $h$. Since $h(x)$ is the longest such run, $h(x)>y$ holds exactly when some $n<x$ starts a run of $H>y$ distinct gaps. We state the question this way, with $x$ real. We read it as asking for one $c>0$ such that the inequality holds for all large $x$.

The primes are indexed from $p_0=2$, as in primeGap. Shifting the index by one does not change the question.

erdos_852.parts.ii. Let $d_n=p_{n+1}-p_n$, where $p_n$ is the $n$th prime. Let $h(x)$ be maximal such that for some $n<x$ the numbers $d_n,d_{n+1},\dots ,d_{n+h(x)-1}$ are all distinct [Er85c]. Estimate $h(x)$. In particular, is it true that $$h(x)=o(\log x)?$$

The statement avoids defining $h$. It says that for every $\epsilon >0$ and all large real $x$, every run of $H$ distinct gaps $d_n,\dots ,d_{n+H-1}$ with $n<x$ satisfies $H\le \epsilon \log x$. This is $h(x)\le \epsilon \log x$, because $h(x)$ is the longest such run.

The indexing is as in Erdos852.erdos_852.parts.i.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«852» (2 statements).

theorem erdos_852.parts.i :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ x : ℝ in atTop,
      ∃ n : ℕ, (n : ℝ) < x ∧ ∃ H : ℕ, (Real.log x) ^ c < (H : ℝ) ∧ DistinctGapRun n H

theorem erdos_852.parts.ii :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
      ∀ n : ℕ, (n : ℝ) < x → ∀ H : ℕ, DistinctGapRun n H → (H : ℝ) ≤ ε * Real.log x

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/852. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/852
• [Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984) (1985), 74-84.
• A001223
• A053597
• A078515

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.