Transcendence of the binary sum $\sum 1/2^{a_n}$ when $\limsup a_n/n=\infty$ (Erdős #247)
Statement
Let $1\le a_1<a_2<\cdots$ be a strictly increasing sequence of integers with $$\limsup_n \frac{a_n}{n}=\infty.$$ Is $$\sum_{n=1}^\infty \frac{1}{2^{a_n}}$$ necessarily transcendental?
Acceptance. FULLY RESOLVES: a proof that every strictly increasing integer sequence with $\limsup a_n/n=\infty$ makes $\sum_n 1/2^{a_n}$ transcendental, OR an explicit such sequence for which the sum is algebraic, with its minimal polynomial certified. A machine-checkable Lean 4 proof extending ErdosProblems/247.lean is the gold standard; otherwise a complete written proof with every step. ADVANCES: a result strictly between the known theorem and the target — e.g. prove Erdős's suggested milestone that $a_n>cn^2$ implies $\sum 1/2^{a_n}$ is not a quadratic irrational, or establish transcendence under a hypothesis strictly weaker than '$\limsup a_n/n^t=\infty$ for all $t\ge 1$' yet stronger than '$\limsup a_n/n=\infty$', with proof. Deliver the Lean proof file or manuscript, or the explicit algebraic counterexample.
Background
Posed by Erdős and Graham [ErGr80, p.61] and reiterated by Erdős in [Er88c, p.106]; listed as open on erdosproblems.com/247 (fetched 2026-07-13, status 'open', tagged 'number theory | irrationality'). Erdős [Er75c] proved the answer is yes under the stronger hypothesis $\limsup a_n/n^t=\infty$ for every $t\ge 1$ (super-polynomially large gaps occurring infinitely often); the problem asks to weaken this to the single condition $\limsup a_n/n=\infty$. Erdős remarked in [Er88c] that many such problems 'seem hopeless at present', but suggested a more tractable milestone: proving that $a_n>cn^2$ forces $\sum 1/2^{a_n}$ to not be a root of any quadratic polynomial (i.e. not a quadratic irrational). Concretely, $\sum 1/2^{a_n}$ is the real number whose binary expansion has a 1 exactly at each position $a_n$, so $\limsup a_n/n=\infty$ says the 1-digits have unbounded average gaps. The statement is formalised in Lean (DeepMind Formal Conjectures, ErdosProblems/247.lean). Attacker's tool: transcendence methods for lacunary binary expansions (Roth / Ridout-type approximation, subword-complexity and automatic-sequence criteria), ideally certified via the existing Lean 4 formalisation.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #247 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #247 (DeepMind Formal Conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.