Erdős Problem 1003

Reference: erdosproblems.com/1003

theorem Erdos1003.erdos_1003 : {n : ℕ | n.totient = (n + 1).totient}.Infinite ↔ sorry

Are there infinitely many solutions to $\phi(n) = \phi(n+1)$, where \phi is the Euler totient function?

theorem Erdos1003.erdos_1003.variants.Icc : (∀ k ≥ 1, {n : ℕ | ∀ i ∈ Set.Icc 1 k, n.totient = (n + i).totient}.Infinite) ↔ sorry

Erdős [Er85e] says that, presumably, for every $k \geq 1$ the equation $$\phi(n) = \phi(n+1) = \cdots = \phi (n+k)$$ has infinitely many solutions.

[Er85e] Erdős, P., Some problems and results in number theory. Number theory and combinatorics. Japan 1984 (Tokyo, Okayama and Kyoto, 1984) (1985), 65-87.

theorem Erdos1003.erdos_1003.variants.eps87 (x : ℝ) : ∃ c > 0, ↑{n : ℕ | ↑n ≤ x ∧ n.totient = (n + 1).totient}.ncard ≤ x / Real.exp (c * Real.log x ^ (1 / 3))

Erdős, Pomerance, and Sárközy [EPS87] proved that the number of $n \leq x$ with $\phi(n) = \phi(n+1)$ is at most $$\frac{x}{\exp(c(\log x)^{1/3})}$$ for some constant $c > 0$.

[EPS87] Erd\H os, Paul and Pomerance, Carl and S'ark"ozy, Andr'as, On locally repeated values of certain arithmetic functions. {III}. Proc. Amer. Math. Soc. (1987), 1--7.