lean_workbook_plus_74810

Disproved

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

Prove that for all positive integers $n$ , $\sqrt{n} + \sqrt{n+2} > 2\sqrt{n + 0.8}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74810 : ∀ n : ℕ, (Real.sqrt n + Real.sqrt (n + 2) : ℝ) > 2 * Real.sqrt (n + 0.8)   :=  by sorry

Source