Erdős problem 258

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$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

258.lean

Retained formal statement3 of 3

Let $2 \leq a_1 \leq a_2 \leq \cdots$ be a monotone sequence with $a_n \to \infty$ . Is $\sum_n \frac{d(n)}{a_1 \cdots a_n}$ irrational, where $d(n)$ is the number of divisors of $n$ ?

Solution: True (proved by Erdős and Straus [ErSt71], Lemma 2.2 and Theorem 2.13).

FormalConjectures/ErdosProblems/258.leanErdos258.erdos_258.variants.monotone6 linesExact file

1True ↔2  ∀ (a : ℕ → ℕ),3    (∀ (n : ℕ), 2 ≤ a n) →4      Monotone a →5        Filter.Tendsto a Filter.atTop Filter.atTop →6          Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 (n + 1), a i))

SolvedStatement only, no proof