lean_workbook_plus_27794

Proved

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

prove that \n\n $\left( x+y+z \right) \left( -2\, \left( x+y+z \right) xyz+ \left( xy+zx+yz \right) ^{2} \right) -2\, \left( xy+zx+yz \right) xyz\geq {x}^{2}{z}^{3}+{x}^{3}{y}^{2}+{y}^{3}{z}^{2}$ \n\n $x,y,z>0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27794 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x + y + z) * (-(2 * (x + y + z) * x * y * z) + (x * y + y * z + z * x) ^ 2) - 2 * (x * y + y * z + z * x) * x * y * z ≥ x ^ 2 * z ^ 3 + x ^ 3 * y ^ 2 + y ^ 3 * z ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph