Irrationality sequences: is $2^{2^n}$ one, and must every such sequence satisfy $a_n^{1/n}\to\infty$? (Erdős #263)
Statement
An increasing sequence of positive integers $a_1<a_2<\cdots$ is called an *irrationality sequence* if, for every sequence of positive integers $b_n$ with $b_n/a_n\to 1$, the sum $$\sum_n \frac{1}{b_n}$$ is irrational. Two questions are asked: (i) Is $a_n=2^{2^n}$ an irrationality sequence? (ii) Must every irrationality sequence satisfy $a_n^{1/n}\to\infty$?
Acceptance. FULLY RESOLVES: settle BOTH questions. For (i): a proof that $\sum 1/b_n$ is irrational for every $b_n$ with $b_n/2^{2^n}\to 1$, or an explicit sequence $b_n$ with $b_n/2^{2^n}\to 1$ for which $\sum 1/b_n$ is rational (with the rational value certified). For (ii): a proof that every irrationality sequence has $a_n^{1/n}\to\infty$, or an explicit irrationality sequence with $\liminf a_n^{1/n}<\infty$. A machine-checkable Lean 4 proof extending ErdosProblems/263.lean is the gold standard; otherwise a complete written proof with every step. ADVANCES: settle either (i) or (ii) alone with proof; or resolve the boundary case left open by Kovač-Tao — e.g. decide the property for the class $a_{n+1}/a_n^2\to c$ for a constant $c>0$, strictly improving on their '$\to 0$ implies not an irrationality sequence' result stated in the background, with proof or reproducible certificate. Deliver the Lean proof file or full manuscript, or the explicit rational-making $b_n$.
Background
Posed by Erdős and Graham [ErGr80, p.63] and reiterated by Erdős in [Er88c, p.105]; listed as open on erdosproblems.com/263 (fetched 2026-07-13, status 'open', tagged 'irrationality'). This is one of several competing definitions of an 'irrationality sequence' — compare the sibling problems Erdős #262 (erdosproblems.com/262) and Erdős #264 (erdosproblems.com/264). A folklore result gives that $\sum 1/a_n$ is irrational whenever $\lim a_n^{1/2^n}=\infty$; consequently, if $\liminf a_{n+1}/a_n^{2+\epsilon}>0$ for some $\epsilon>0$ then $a_n$ is an irrationality sequence. Kovač and Tao [KoTa24] proved that any strictly increasing sequence with $\sum 1/a_n$ convergent and $\lim a_{n+1}/a_n^2=0$ is NOT an irrationality sequence — this eliminates slowly growing candidates but leaves $a_n=2^{2^n}$ (for which $a_{n+1}/a_n^2=1$, exactly on the boundary) undecided. Koizumi [Ko25c] proved that $a_n=\lfloor\alpha^{2^n}\rfloor$ is an irrationality sequence for all but countably many $\alpha>1$; the specific value $\alpha=2$, giving $2^{2^n}$, could lie in the countable exceptional set, so this does not settle (i). The problem was originally stated without the 'increasing' hypothesis, under which DeepMind produced a counterexample, prompting the corrected statement above. The statement is formalised in Lean in the DeepMind Formal Conjectures project (ErdosProblems/263.lean). Attacker's tool: Diophantine/analytic irrationality machinery (approximation-exponent and partial-quotient bounds for perturbed reciprocal series), ideally certified by extending the existing Lean 4 formalisation.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #263 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #263 (DeepMind Formal Conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.