A strict rational lower bound for a quadratic recurrence

Proved

WorkbookCorrected.plus_13202

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Prove that for the sequence $\{x_n\}$ defined by $x_1=\frac 12, \ x_{n+1}=x_n+\left(\frac{x_n}n\right)^2$ , we have $x_n>\frac{6n}{5n+6}, \forall n\geq 3$ .

Formalization Note: The recurrence is restricted to positive indices, as in the source sequence starting at1. The complete lower bound is proved for every n≥3.

Source: InternLM Lean-Workbook, record lean_workbook_plus_13202 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_13202 (x : ℕ → ℝ) (hx : x 1=1/2)
    (h : ∀ n : ℕ, 1≤n → x (n+1)=x n+(x n/(n:ℝ))^2) :
    ∀ n : ℕ, 3≤n → x n > 6*(n:ℝ)/(5*(n:ℝ)+6) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_13202; Apache-2.0

View graph