Prove2Me

lean_workbook_plus_11423

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let x1∈<0,1>x_1 \in <0,1> and define xn+1=xn+xn2n2x_{n+1}=x_n +\frac{x_{n}^{2}}{n^2} . Prove that the sequence xnx_n is bounded.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11423 (x : ℕ → ℝ) (hx: ∀ n, 0 < x n ∧ x n < 1) (hn: ∀ n, x (n + 1) = x n + (x n)^2 / n^2): ∃ M, ∀ n, abs (x n) < M   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph