Prove2Me

lean_workbook_plus_40167

Proved

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

Prove that (a2+b2)2≥(a+b+c)(a+b−c)(b+c−a)(c+a−b)(a^2 + b^2)^2 \geq (a + b + c)(a + b - c)(b + c - a)(c + a - b) using the inequality xy≤(x+y)24xy \leq \frac{(x+y)^2}{4} for all x,y∈Rx, y \in \mathbb{R}.

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

View graph