Lehmer's totient problem

Reference: Wikipedia

theorem lehmer_totient : (∃ n > 1, ¬Prime n ∧ n.totient ∣ n - 1) ↔ sorry

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