Prove2Me

lean_workbook_plus_54808

Proved

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

(a2+b2)2≥(a+b+c)(a+b−c)(b+c−a)(c+a−b)\left(a^2 + b^2\right)^2 \geq (a + b + c)(a + b - c)(b + c - a)(c + a - b)   ⟺  \iff \n\n (a2+b2−c2)2+(a2−b2)2≥0\left(a^2+b^2-c^2\right)^2+\left(a^2-b^2\right)^2\ge 0 with equality iff ∣a∣1=∣b∣1=∣c∣2\frac {|a|}{1}=\frac {|b|}{1}=\frac {|c|}{\sqrt 2}

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

View graph