Erdős Problem 247

Reference: erdosproblems.com/247

theorem erdos_247 : (∀ (n : ℕ → ℕ), StrictMono n → Filter.limsup (fun (k : ℕ) => ↑(n k) / ↑k.succ) Filter.atTop = ⊤ → Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)) ↔ sorry

Let $n_1 < n_2 < \cdots$ be a sequence of integers such that $$ \limsup \frac{n_k}{k} = \infty. $$ Is $$ \sum_{k=1}^{\infty} \frac{1}{2^{n_k}} $$ transcendental?

theorem erdos_247.variants.strong_condition (n : ℕ → ℕ) (hn : StrictMono n) (h : ∀ t ≥ 1, Filter.limsup (fun (k : ℕ) => ↑(↑(n k) / ↑k.succ ^ t)) Filter.atTop = ⊤) : Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)

Erdős proved the answer is yes under the stronger condition that $\limsup \frac{n_k}{k^t} = \infty$ for all $t\geq 1$.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).