Erdős Problem 243

Reference: erdosproblems.com/243

theorem erdos_243 (a : ℕ → ℕ) (ha₀ : StrictMono a) (ha₁ : Filter.Tendsto (fun (n : ℕ) => ↑(a n) / ↑(a (n - 1)) ^ 2) Filter.atTop (nhds 1)) (ha₂ : Summable fun (x : ℕ) => 1 / ↑(a x)) : ∀ᶠ (n : ℕ) in Filter.atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

Let $a_1 < a_2 < \dots$ be a sequence of integers such that $\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1$ and $\sum \frac{1}{a_n} \in \mathbb{Q}$.

Then, for all sufficiently large $n \ge 1$, $a_n = a_{n-1}^2 - a_{n-1} + 1$.