Prove2Me

lean_workbook_plus_22065

Proved

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

For any real number 0≤x≤40 \le x \le 4 ,

x≥x2\sqrt{x} \ge \frac{x}{2}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22065 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 4) : Real.sqrt x ≥ x / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph