Erdős Problem 263

Reference: erdosproblems.com/263

def Erdos263.IsIrrationalitySequence (a : ℕ → ℕ) : Prop

We call a sequence $a_n$ of positive integers an irrationality sequence if for any sequence $b_n$ of positive integers with $\frac{a_n}{b_n} \to 1$ as $n \to \infty$, the sum $\sum \frac{1}{b_n}$ converges to an irrational number.

Note: This is one of many possible notions of "irrationality sequences". See FormalConjectures/ErdosProblems/264.lean for another possible definition.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos263.erdos_263.parts.i : sorry ↔ IsIrrationalitySequence fun (n : ℕ) => 2 ^ 2 ^ n

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

theorem Erdos263.erdos_263.parts.ii : sorry ↔ ∀ (a : ℕ → ℕ), IsIrrationalitySequence a → Filter.Tendsto (fun (n : ℕ) => ↑(a n) ^ (1 / ↑n)) Filter.atTop Filter.atTop

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

theorem Erdos263.erdos_263.variants.folklore (a : ℕ → ℕ) (ha : Filter.Tendsto (fun (n : ℕ) => ↑(a n) ^ (1 / 2 ^ n)) Filter.atTop Filter.atTop) : Irrational (∑' (n : ℕ), 1 / ↑(a n))

A folklore result states that any $a_n$ satisfying $\lim_{n \to \infty} a_n^{\frac{1}{2^n}} = \infty$ has $\sum \frac{1}{a_n}$ converging to an irrational number.

theorem Erdos263.erdos_263.variants.sub_doubly_exponential (a : ℕ → ℕ) (ha' : StrictMono a) (ha'' : Summable fun (n : ℕ) => 1 / ↑(a n)) (ha''' : Filter.Tendsto (fun (n : ℕ) => ↑(a (n + 1)) / ↑(a n) ^ 2) Filter.atTop (nhds 0)) : ¬IsIrrationalitySequence a

Kovač and Tao [KoTa24] proved that any strictly increasing sequence $a_n$ such that $\sum \frac{1}{a_n}$ converges and $\lim \frac{a_{n+1}}{a_n^2} = 0$ is not an irrationality sequence in the above sense.

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem Erdos263.erdos_263.variants.super_doubly_exponential (a : ℕ → ℕ) (ha : ∀ (n : ℕ), a n > 0) (ha' : StrictMono a) (ha'' : ∃ ε > 0, Filter.liminf (fun (n : ℕ) => ↑(a (n + 1)) / ↑(a n) ^ (2 + ε)) Filter.atTop > 0) : IsIrrationalitySequence a

On the other hand, if there exists some $\varepsilon > 0$ such that $a_n$ satisfies $\liminf \frac{a_{n+1}}{a_n^{2+\varepsilon}} > 0$, then $a_n$ is an irrationality sequence by the above folklore result erdos_263.variants.folklore.

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

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).