Erdős Problem 258

References:

• erdosproblems.com/258
• [Ch26] P. Chojecki and GPT-5.4 Pro, Erdős problem 258 (2026)
• [St26] ster-oc, Lean formalisation of Erdős problem 258 (2026)

theorem Erdos258.erdos_258 : 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))

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

This was proved affirmatively by Chojecki and GPT-5.4 Pro [Ch26], and formalised in Lean by ster-oc [St26].

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

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).

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

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)