Erdős Problem 259

Reference: erdosproblems.com/259

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

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

This is true, and was proved by Chen and Ruzsa.

[ChRu99] Chen, Yong-Gao and Ruzsa, Imre Z., On the irrationality of certain series. Period. Math. Hungar. (1999), 31--37.