Erdős Problem 251

Reference: erdosproblems.com/251

theorem Erdos251.erdos_251 : Irrational (∑' (n : ℕ), ↑(Nat.nth Nat.Prime n) / 2 ^ n) ↔ sorry

Is $$\sum_{n} \frac{p_n}{2^n}$$ irrational? Here $p_n$ is the $n$-th prime. With the convention $p_1 = 2$, the sum in the formal statement is half the sum in the informal statement, which doesn't influence the irrationality.