Erdős Problem 828

Reference: erdosproblems.com/828

theorem Erdos828.erdos_828 : sorry ↔ ∀ (a : ℤ), {n : ℕ | ↑n.totient ∣ ↑n + a}.Infinite

Is it true that, for any $a \in \mathbb{Z}$, there are infinitely many $n$ such that $$\phi(n) | n + a$$?

theorem Erdos828.erdos_828.variants.lehmer_conjecture : sorry ↔ ∀ n > 1, n.totient ∣ n - 1 ↔ Prime n

When $n > 1$, Lehmer conjectured that $\phi(n) | n - 1$ if and only if $n$ is prime.

theorem Erdos828.erdos_828.variants.phi_dvd_self_iff_pow2_pow3 {n : ℕ} : n.totient ∣ n ↔ n ≤ 1 ∨ ∃ a > 0, ∃ (b : ℕ), n = 2 ^ a * 3 ^ b

It is an easy exercise to show that $\phi(n) | n$ if and only if $n = 0, 1$ or $n = 2^a 3^b$ for some $a > 0$.