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.$

Worked, still open.

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

use this record

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

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 ↗

oeis

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

links

Sylvester's sequence · reference

#315Let

u_{1} = 1

and

u_{n + 1} = u_{n} (u_{n} + 1)

, so that

\sum_{k \geq 1} \frac{1}{u _{k} + 1}

and

u_{k} = ⌊ c_{0}^{2^{k}} + 1 ⌋

for

k \geq 1

, where

c_{0} = lim u_{n}^{1/ 2^{n}} = 1.264085 \dots .

Let

a_{1} < a_{2} < \dots

be any other sequence with

\sum \frac{1}{a _{k}} = 1

. Is it true that

lim inf a_{n}^{1/ 2^{n}} < c_{0} = 1.264085 \dots ?

A000058

status