Erdős Problem 249

Reference: erdosproblems.com/249

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

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