Sequences & series · Last catalog review 26 Jul 2026

Erdős Problem 243

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

References

erdosproblems.com/243

Published 10 Jun 2026Never attempted

Formal statement

Lean type

∀ (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

What you must prove

import FormalConjectures.ErdosProblems.«243»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos243.erdos_243" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/243.lean

Source type SHA-256: sha256:ba32c2cf4a6115f9b6f592a10cfc4eb7e93182059efa2302ca69a211ced3ec3f
Task id: fc-e923379e-erdos243-erdos-243-70efa0eb38-formalized-v1
Task commitment: sha256:74e6f47585073a2402f4f83ad5ade955d1a9fcc83bb176ede1412315b8490214

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.