lean_workbook_plus_54172

Proved

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

We need to prove that $(x^2+y^2+z^2)^3\geq(x+y+z)^2(x^2+y^2+z^2-xy-xz-yz)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54172 (x y z : ℝ) :
  (x^2 + y^2 + z^2)^3 ≥ (x + y + z)^2 * (x^2 + y^2 + z^2 - x * y - x * z - y * z)^2   :=  by sorry

Source