lean_workbook_plus_57680

Disproved

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

prove that: $x^2(x+y)(x+z)+y^2(y+x)(y+z)+z^2(z+x)(z+y)\geq 1+(x+y)^2+(x+z)^2+(y+z)^2$ given $x,y,z>0$ and $x+y+z=1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57680 : ∀ x y z : ℝ, x + y + z = 1 → x > 0 ∧ y > 0 ∧ z > 0 → x^2 * (x + y) * (x + z) + y^2 * (y + x) * (y + z) + z^2 * (z + x) * (z + y) ≥ 1 + (x + y)^2 + (x + z)^2 + (y + z)^2   :=  by sorry

Source

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

View graph