Erdős problem 1004
For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c. This is an open problem.
Sources
FormalConjectures/ErdosProblems/
1004.lean
Retained formal statement
Erdős, Pomerance, and Sárközy [EPS87] proved that if φ(n+k) are all distinct for 1 ≤ k ≤ K then K ≤ n / exp(c (log n)^{1/3}) for some constant c > 0. Here we state the existence of such a constant c.
True ↔ ∃ c, ∃ (_ : c > 0), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (K : ℕ), Erdos1004.IsDistinctTotientRun n K → ↑K ≤ ↑n / Real.exp (c * Real.log ↑n ^ (1 / 3))SolvedStatement only, no proof