---

Hančl, Jaroslav, Expression of real numbers with the help of infinite series, Acta Arith. 59 (1991), no. 2, 97–104. Call an increasing sequence of positive integers $a_n$ an irrationality sequence when $\sum 1/(t_na_n)$ is irrational for every choice of integers $t_n\ge1$. Hančl's Corollary 2 states that every sequence of positive reals $c_n$ with

$$\limsup_{n\to\infty}\frac{\log_2\log_2 c_n}{n}<1$$

is a rational sequence: some choice of positive integers $b_n$ makes $\sum 1/(c_nb_n)$ rational. An irrationality sequence therefore satisfies $\limsup(\log_2\log_2 a_n)/n\ge1$. His Theorem 2 and Corollary 1 give the finer exclusion the site records: if $a_n\ll 2^{2^{n-F(n)}}$ with $F(n)<n$ and $\sum 2^{-F(n)}<\infty$, then $a_n$ is not an irrationality sequence. The proofs run a greedy induction choosing the factors $b_n$ one at a time so that the remainder of a target rational is driven to zero. Erdős had shown in the 1975 paper the site cites that $a_n=2^{2^n}$ is an irrationality sequence (source card), so the answer to how slowly $a_n$ can grow is: doubly exponentially, with $\limsup(\log_2\log_2 a_n)/n=1$ attained and nothing below it possible. The source card digests the paper. Hančl remarks that he does not know whether $2^{2^n/n}$ is a rational sequence, so the exact boundary at the threshold is not described.

Acceptance. Refereed: Acta Arithmetica, volume 59, issue 2 (1991). Reviewed: the erdosproblems.com page for Problem 262 (last edited 2025-09-28) is labeled "SOLVED (LEAN)" by the site's curator, Thomas Bloom, who writes that Hančl essentially solved the problem and states his bound; as of 2026-10-07 the problem's forum thread carries no comment and its proof-claims tab no entry. This corpus has not reproved the theorem and awards no tier of its own.

Formalization. A public Lean 4 development in Boris Alexeev's lean-proofs repository declares itself a formalization of Hančl's solution, names him as the informal author and lists Codex and GPT-5.6 Sol as its formal authors; its theorem erdos_262, at the linked line of the commit of 2026-09-15, states that every irrationality sequence, defined there as a positive strictly increasing sequence with all $t_n\ge1$, has $\limsup(\log_2\log_2 a_n)/n\ge1$ in the extended reals. The file entered the repository on 2026-08-17, and the community database has recorded a Lean formal status for the problem as of that field's last update on 2026-08-24, without recording when that state was set, naming no proof; formal-conjectures holds no statement file for the problem. As of that date the corpus records no build or audit of the development and no check of its statement against the problem's formulation, so the formalization is a link and not acceptance evidence.

Depends on. Erdős's example, the accepted partial claim that $2^{2^n}$ is an irrationality sequence, which supplies the attained half of the answer; otherwise the claim rests on the cited paper.