Erdős problem 263

Must every irrationality sequence $a_n$ in the above sense satisfy $a_n^{1/n} \to \infty$ as $n \to \infty$ ?

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

263.lean

Retained formal statement3 of 6

Koizumi [Ko25] showed that $a_n = \lfloor \alpha^{2^n} \rfloor$ is an irrationality sequence for all but countably many $\alpha > 1$ .

[Ko25] Koizumi, J., Irrationality of the reciprocal sum of doubly exponential sequences, arXiv:2504.05933 (2025).

FormalConjectures/ErdosProblems/263.leanErdos263.erdos_263.variants.doubly_exponential_all_but_countable1 lineExact file

1∀ᶠ (α : ℝ) in Filter.cocountable, α > 1 → Erdos263.IsIrrationalitySequence fun n => ⌊α ^ 2 ^ n⌋₊

SolvedStatement only, no proof