ErdosProblems · research open · AMS 40

unsolvedsorry — nobody on it

Erdős Problem 243

Conjecture 243 · Erdős

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.

Formal statement · Lean 4.lean
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 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗