Prove2Me

lean_workbook_plus_37925

Proved

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

Given the finite sequence\n\nak=ak−1+ak−12na_k= a_{k-1}+ \frac{a^2_{k-1}}{n} ; k∈[1;n]k \in [1;n]\n\nProve that\n\n1−1n<an<11- \frac{1}{n}<a_n<1\n\na0=12a_0 = \frac{1}{2}

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

View graph