Erdős problem 258 · problems.science

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/258.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:258
PLBY Lean proofsErdosProblems.Erdos258

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI building on literature
Erdős AI contributions wiki · 14 Apr, 2026
Machine
GPT-5.4 Pro
Open the source record
Formalization
Erdős AI contributions wiki · 14 Apr, 2026
Machine
Aristotle
Open the source record
argument
VibeMathed
Machine
GPT-5.4 Pro
Reported outcome
resolved
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science