Erdős Problem 258

Reference: erdosproblems.com/258

theorem erdos_258 : (∀ (a : ℕ → ℕ), (∀ (n : ℕ), a n ≠ 0) → Filter.Tendsto a Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 n, a i))) ↔ sorry

Let $a_n \to \infty$ be a sequence of non-zero natural numbers. Is $\sum_n \frac{d(n)}{(a_1 ... a_n)}$ irrational, where $d(n)$ is the number of divisors of $n$?

theorem erdos_258.variants.Monotone : (∀ (a : ℕ → ℤ), (∀ (n : ℕ), a n ≠ 0) → _root_.Monotone a → Filter.Tendsto a Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 n, a i))) ↔ True

Let $a_n \to \infty$ be a monotone sequence of non-zero natural numbers. Is $\sum_n \frac{d(n)}{(a_1 ... a_n)}$ irrational, where $d(n)$ is the number of divisors of $n$?

Solution: True (proved by Erdős and Straus, see Erdős Problems website).

theorem erdos_258.variants.Constant : (∀ t ≥ 2, Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / t ^ n)) ↔ True

Is $\sum_n \frac{d(n)}{t^n}$ irrational, where $t ≥ 2$ is an integer.

Solution: True (proved by Erdős, see Erdős Problems website)