Prove2Me

lean_workbook_plus_59795

Proved

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

b2+42≥b+22\sqrt{\frac{b^{2}+4}{2}}\geq \frac{b+2}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59795 (b : ℝ) : Real.sqrt ((b^2 + 4)/2) ≥ (b + 2)/2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph