Prove2Me

lean_workbook_plus_13371

Proved

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

Prove (a+b2)2>ab,a≠b\left ( {\frac{a+b}{2}} \right )^2 > ab, \quad a \ne b

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13371 (a b : ℝ) (hab : a ≠ b) : (a + b) ^ 2 / 4 > a * b   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph