Prove2Me

lean_workbook_plus_19903

Disproved

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

More stronger is: \n (x2+y2)(y2+z2)(x2+z2)(xy+xz+yz)2(x+y+z)2≥8 (xy2+yz2+x2z)2(x2y+y2z+z2x)2 \left( {x}^{2}+{y}^{2} \right) \left( {y}^{2}+{z}^{2} \right) \left( {x}^{2}+{z}^{2} \right) \left( xy+xz+yz \right) ^{2} \left( x+y+z \right) ^{2}\geq 8\, \left( x{y}^{2}+y{z}^{2}+{x}^{2}z \right) ^{2} \left( {x}^{2}y+{y}^{2}z+{z}^{2}x \right) ^{2}

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

View graph