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

Open selected source

FormalConjectures/ErdosProblems/

258.lean

Retained formal statement1 of 3

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

FormalConjectures/ErdosProblems/258.leanErdos258.erdos_2585 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.