Erdős Problem 259

Reference: erdosproblems.com/259

theorem Erdos259.erdos_259 : Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.moebius n) ^ 2 * ↑n / 2 ^ n) ↔ sorry

Is $$\sum_{n} \mu(n)^2\frac{n}{2^n}$$ irrational?