The board / irrationality / #258
Erdős Problem #258
PROVED LEANdatabase updated 2026-04-21
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
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].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/258.Prizenone
Topicsirrationality
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/258
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.