Prove2Me

lean_workbook_plus_21731

Proved

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

Show that (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_21731 (a b : ℝ) (h1 : a ≠ b) (h2 : a ≠ -b) : (a + b) ^ 2 / 4 > a * b   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph