Erdős Problem 828

Reference: erdosproblems.com/828

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

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 : (∀ n > 1, n.totient ∣ n - 1 ↔ Prime n) ↔ sorry

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 > 1 → (n.totient ∣ n ↔ ∃ (a : ℕ) (b : ℕ), n = 2 ^ a * 3 ^ b)

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