Erdős Problem 822

Does the set of integers of the form n + φ(n) have positive (lower) density? Gabdullin, Iudelevich, and Luca proved this was true.

Reference: erdosproblems.com/822

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

Erdős Problem 822.

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

The problem is known to have an affirmative answer.