Let $a_1,a_2,\dots$ be a sequence of positive integers with $a_n\to \infty$. Is$$\sum _n\frac{\tau (n)}{a_1\cdots a_n}$$irrational, where $\tau (n)$ is the number of divisors of $n$?

AMS 11 · solved (literature)

theorem erdos_258 : answer(True) ↔ ∀ (a : ℕ → ℕ), (∀ n, 2 ≤ a n) →
    Filter.Tendsto a Filter.atTop Filter.atTop →
    Irrational (∑' (n : ℕ), ((n + 1).divisors.card / ∏ i ∈ Finset.Icc 1 (n + 1), a i))