lean_workbook_plus_2618

Proved

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

It suffices to prove that ${({a^2} + {b^2} + {c^2})^2} \ge \left[ {a(a - b + c) + b(b - c + a) + c(c - a + b)} \right]^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2618 : ∀ a b c : ℝ, (a^2 + b^2 + c^2)^2 ≥ (a * (a - b + c) + b * (b - c + a) + c * (c - a + b))^2   :=  by sorry

Source