Erdős problem 247

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?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

247.lean

Retained formal statement1 of 2

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?

FormalConjectures/ErdosProblems/247.leanErdos247.erdos_2474 linesExact file

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

OpenStatement only, no proof