Erdős Problem 257

Reference: erdosproblems.com/257

theorem erdos_257 : (∀ (A : Set ℕ), A.Infinite → Irrational (∑' (n : ↑A), 1 / (2 ^ ↑n - 1))) ↔ sorry

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

theorem erdos_257.variants.tsum_top_eq : ∑' (n : ℕ), 1 / (2 ^ n - 1) = ∑' (n : ℕ), ↑n.divisors.card / 2 ^ n

Show that $$ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, $$ where $d(n)$ is the number of divisors of $n$.

theorem erdos_257.variants.tsum_top : Irrational (∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)

Show that $$ \sum_{n} \frac{d(n)}{2^n} $$ is irrational.

[Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.