Erdős problem 260
Let be an increasing sequence such that . Is the sum irrational?
Sources
FormalConjectures/ErdosProblems/
260.lean
Retained formal statement
Let be an increasing sequence such that . Is the sum irrational?
sorry ↔ ∀ (a : ℕ → ℤ) (s : ℝ), StrictMono a → Filter.Tendsto (fun n => ↑(a n) / ↑n) Filter.atTop Filter.atTop → HasSum (fun n => ↑(a n) / 2 ^ a n) s → Irrational sOpenStatement only, no proof