Is it true that if $a_0 1$, then the series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$ is irrational?

Erdős problem 1051

Start work

Is it true that if $a_0 < a_1 < a_2 < \cdots$ is a strictly increasing sequence of integers with $\liminf a_n^{1/2^n} > 1$ , then the series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$ is irrational?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1051.lean

Retained formal statement2 of 2

Erdős [Er88c] notes that if the sequence grows rapidly to infinity (specifically, if $a_{n+1} \geq C \cdot a_n^2$ for some constant $C > 0$ ), then the series is irrational.

FormalConjectures/ErdosProblems/1051.leanErdos1051.erdos_1051.variants.rapid_growth1 lineExact file

1∀ (a : ℕ → ℤ), StrictMono a → (∃ C > 0, ∀ (n : ℕ), ↑(a (n + 1)) ≥ C * ↑(a n) ^ 2) → Irrational (Erdos1051.ErdosSeries a)

SolvedStatement only, no proof