lean_workbook_plus_41129

Disproved

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

Prove that $4n + 1 < (\sqrt{n} + \sqrt{n+1})^2 < 4n + 3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41129 : ∀ n : ℕ, 4 * n + 1 < (Real.sqrt n + Real.sqrt (n + 1))^2 ∧ (Real.sqrt n + Real.sqrt (n + 1))^2 < 4 * n + 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph