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 statement1 of 6

Is $a_n = 2^{2^n}$ an irrationality sequence in the above sense?

FormalConjectures/ErdosProblems/263.leanErdos263.erdos_263.parts.i1 lineExact file

1sorry ↔ Erdos263.IsIrrationalitySequence fun n => 2 ^ 2 ^ n

OpenStatement only, no proof