Erdős Problem 249

Reference: erdosproblems.com/249

theorem Erdos249.erdos_249 : True ↔ Irrational (∑' (n : ℕ), ↑n.totient / 2 ^ n)

Is $$\sum_{n} \frac{\phi(n)}{2^n}$$ irrational? Here $\phi$ is the Euler totient function.