Erdős Problem 260

Reference: erdosproblems.com/260

theorem Erdos260.erdos_260 : True ↔ ∀ (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 s

Let $a_1 < a_2 < \cdots$ be an increasing sequence such that $\frac{a_n}{n} \to \infty$. Is the sum $\sum_{n}^{\infty} \frac{a_n}{2^{a_n}}$ irrational?