Prove2Me

lean_workbook_plus_33014

Proved

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

n+n+2<n+1+1\sqrt{\sqrt{n}+n+2} < \sqrt{n+1}+1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33014 (n : ℕ) : Real.sqrt (Real.sqrt n + n + 2) < Real.sqrt (n + 1) + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph