lean_workbook_plus_33515

Disproved

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

Define a sequence $<x_{n}>$ by $x_{1}=1,x_{n}=x_{n-1}+\frac{1}{x_{n-1}}$ , for $n\geq 2$ . Show that $12\leq x_{15}\leq 15$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33515 (x : ℕ → ℝ) (x1 : x 0 = 1) (xn : ∀ n, x (n + 1) = x n + 1 / x n) : 12 ≤ x 15 ∧ x 15 ≤ 15   :=  by sorry

Source