lean_workbook_plus_32146

Proved

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

Given a sequence $(x_n)$ defined by $x_1=\frac{1}{2}$ and $x_{n+1}=x_n-x_n^2$ . Prove that $\sum_{1}^{\infty} x_n$ converges.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32146 (x : ℕ → ℝ) (hx : x 1 = 1 / 2 ∧ ∀ n, x (n + 1) = x n - (x n) ^ 2) : Summable x   :=  by sorry

Source