Irrationality of $\sum a_n/2^{a_n}$ for increasing integer sequences with $a_n/n\to\infty$ (Erdős #260)
Statement
Let $a_1<a_2<\cdots$ be a strictly increasing sequence of positive integers such that $a_n/n\to\infty$. Is the sum $$\sum_n \frac{a_n}{2^{a_n}}$$ necessarily irrational? That is, must this series have an irrational value for every such sequence, or does some admissible sequence make it rational?
Acceptance. FULLY RESOLVES: a complete proof — machine-checkable (Lean/Coq) preferred, else a full written proof — that $\sum_n a_n/2^{a_n}$ is irrational for every strictly increasing positive-integer sequence with $a_n/n\to\infty$; OR a counterexample, namely an explicit admissible sequence $(a_n)$ together with a proof that the resulting sum is rational. ADVANCES: prove irrationality under a hypothesis strictly weaker than the best sufficient conditions stated in the background ($a_{n+1}-a_n\to\infty$, or $a_n\gg n\sqrt{\log n\log\log n}$) yet still stronger than $a_n/n\to\infty$, closing part of the gap with proof; or settle the Erdős–Graham sub-question of whether $\limsup(a_{n+1}-a_n)=\infty$ suffices (either direction, with proof). Deliver the proof/formalization or the rational-sum sequence plus its rationality proof.
Background
Posed by Erdős [Er74b] and reiterated by Erdős–Graham [ErGr80], with later appearances in [Er81h, p.180], [Er88c, p.103] and Vardi [Va99, 1.33]; listed as open on erdosproblems.com/260 (fetched 2026-07-21, status 'open'). Erdős [Er81l] proved the sum is irrational under either of two strictly stronger growth hypotheses: (i) $a_{n+1}-a_n\to\infty$, or (ii) $a_n\gg n\sqrt{\log n\log\log n}$. The open case therefore lives between $a_n/n\to\infty$ and the proven threshold $a_n\gg n\sqrt{\log n\log\log n}$. Erdős and Graham further speculate that the weaker condition $\limsup(a_{n+1}-a_n)=\infty$ is NOT sufficient to force irrationality, but know of no counterexample. (The variant Vardi [Va99] states, replacing $a_n/n\to\infty$ by $a_{n+1}-a_n\to\infty$, was already settled affirmatively by Erdős [Er81l].) The statement is formalised in DeepMind's formal-conjectures repository (260.lean). As of the fetch date an unverified proof-claim has been posted in the site's forum thread (/forum/thread/260/proof-claims) but has not been incorporated into Bloom's remarks, and the problem remains listed as open. The attacker's tool: Diophantine/irrationality criteria exploiting the binary gap structure of the exponents, Lean formalization of the known sufficient conditions, and numerical exploration of slowly-growing sequences to probe the Erdős–Graham suspicion.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #260 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #260 (DeepMind formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.