Let $1 \leq a_{1} < a_{2} < \dots$ be a sequence of integers such that $n \to \infty lim \frac{a _{n}}{a _{n - 1}^{2}} = 1$ and $\sum \frac{1}{a _{n}} \in Q$ . Then, for all sufficiently large $n \geq 1$ , $a_{n} = a_{n - 1}^{2} - a_{n - 1} + 1.$

unreviewedOpen. Worked here; no verified result yet.

number theory · open · formalized (Lean) · 0 attempts

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is **exactly Erdős Problem #243**. As of **January 2026**, it is regarded as **open**: no general proof (or counterexample) is known that the two hypotheses

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

Formal proof

AMS 40 · open (literature)

theorem erdos_243 (a : ℕ → ℕ) (ha₀ : StrictMono a)
    (ha₁ : Tendsto (fun n ↦ (a n : ℝ) / a (n - 1) ^ 2) atTop (𝓝 1))
    (ha₂ : Summable ((1 : ℚ) / a ·)) :
      ∀ᶠ n in atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

formal-conjectures/243.lean ↗

OEIS1

A000058 — Sylvester's sequence: a(n+1) = a(n)^2 - a(n) + 1, with a(0) = 2.2,3,7,43,1807,3263443,10650056950807,113423713055421844361000443,12864938683278671740537145998360961546653259485195807

Connections1

Sylvester's sequence · reference

#315Let