Skip to content

Erdős problem 243

Start work

Let a1<a2<…a_1 < a_2 < \dots be a sequence of integers such that lim⁡n→∞anan−12=1\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1 and ∑1an∈Q\sum \frac{1}{a_n} \in \mathbb{Q}.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

243.lean

Retained formal statement1 of 1

Let a1<a2<…a_1 < a_2 < \dots be a sequence of integers such that lim⁡n→∞anan−12=1\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1 and ∑1an∈Q\sum \frac{1}{a_n} \in \mathbb{Q}.

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

FormalConjectures/ErdosProblems/243.leanErdos243.erdos_2434 linesExact file
∀ (a : ℕ → ℕ),  StrictMono a →    Filter.Tendsto (fun n => ↑(a n) / ↑(a (n - 1)) ^ 2) Filter.atTop (nhds 1) →      (Summable fun x => 1 / ↑(a x)) → ∀ᶠ (n : ℕ) in Filter.atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1
OpenStatement only, no proof