Prove2Me

lean_workbook_plus_77811

Disproved

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

prove that \n (3 xyz+x2y+y2z+z2x)2≥4 xyz(x\ny+zx+yz)(x+y+z)\left( 3\,xyz+{x}^{2}y+{y}^{2}z+{z}^{2}x \right) ^{2}\geq 4\,xyz \left( x\ny+zx+yz \right) \left( x+y+z \right) \n

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

View graph