Erdős Problem 822

References:

• erdosproblems.com/822
• [GIL24] Gabdullin, Mikhail R. and Iudelevich, Vitalii V. and Luca, Florian, Numbers of the form {$k+f(k)$}. J. Number Theory (2024), 58--85.

theorem Erdos822.erdos_822 : True ↔ (Set.range fun (n : ℕ) => n + n.totient).HasPosDensity

Does the set of integers of the form $n + \varphi(n)$ have positive (lower) density?

[GIL24] proved this was true.