Prove2Me

lean_workbook_plus_32180

Proved

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

Express the recurrence relation as xn+1=xn(1−xn)(1+xn2)x_{n+1}=x_n(1-x_n)(1+x_n^2) and show that xn∈(0,1)x_n\in (0,1) for all n∈Nn\in\mathbb{N}.

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

View graph