Lehmer's totient problem

Reference: Wikipedia

theorem LehmerTotient.lehmer_totient : True ↔ ∃ n > 1, ¬Prime n ∧ n.totient ∣ n - 1

Does there exist a composite number $n > 1$ such that Euler’s totient function $\varphi(n)$ divides $n - 1$?