Prove2Me

lean_workbook_plus_53745

Proved

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

By Cauchy-Schwarz Inequality, we have \n 2(x2+y2)(y2+z2)(z2+x2)=[(x+y)2+(x−y)2][(xy+z2)2+z2(x−y)2]&⩾[(x+y)(xy+z2)+z(x−y)]2&=[xy(x+y)+yz(y+z)+zx(z+x)−2xyz]2.\begin{aligned}2(x^2+y^2)(y^2+z^2)(z^2+x^2)&=[(x+y)^2+(x-y)^2][(xy+z^2)^2+z^2(x-y)^2] \&\geqslant [(x+y)(xy+z^2)+z(x-y)]^2\&=[xy(x+y)+yz(y+z)+zx(z+x)-2xyz]^2.\end{aligned}

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

View graph