Skip to content

Erdős problem 1004

Start work

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

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1004.lean

Retained formal statement2 of 2

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.

FormalConjectures/ErdosProblems/1004.leanErdos1004.erdos_1004.variants.le_of_isDistinctTotientRun5 linesExact file
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