Erdős Problem 69

Reference: erdosproblems.com/69

theorem Erdos69.erdos_69 : Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))

Is $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} $$ irrational? (Here $\omega(n)$ counts the number of distinct prime divisors of $n$.)

theorem Erdos69.erdos_69.specialisation_of_erdos_257 : let A := {n : ℕ | Nat.Prime n}; ∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2) = ∑' (p : ↑A), 1 / (2 ^ ↑p - 1)

Tao observed that erdos_69 is a special case of erdos_257, since $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} = \sum_p \frac{1}{2^p - 1}. $$