Erdős problem 247
Let be a sequence of integers such that Is transcendental?
Sources
FormalConjectures/ErdosProblems/
247.lean
Retained formal statement
Erdős proved the answer is yes under the stronger condition that for all .
[ErGr80] Erdős, P. and Graham, R., _Old and new problems and results in combinatorial number theory_. Monographies de L'Enseignement Mathematique (1980).
∀ (n : ℕ → ℕ), StrictMono n → (∀ t ≥ 1, Filter.limsup (fun k => ↑(↑(n k) / ↑k.succ ^ t)) Filter.atTop = ⊤) → Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)SolvedStatement only, no proof