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$?

Note: this was answered false for the *pre-correction* statement, which did not require monotonicity — the counterexample sequence is not increasing. The problem was corrected on erdosproblems.com on 2026-04-02 to require increasing sequences; for the corrected statement this question is open. The earlier formal proof (for the pre-correction definition) is preserved at https://github.com/google-deepmind/formal-conjectures/blob/c8cf651906abe91051cf835d4232ad5648412113/FormalConjectures/ErdosProblems/263.lean#L298