Prove2Me

lean_workbook_plus_78570

Disproved

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

prove \n\n (−y2z2+(y+z)3x)(y−z)2+(−z2x2+(z+x)3y)(z−x)2+(−x2y2+(x+y)3z)(x−y)2≥(3+2 2)(x−y)2(y−z)2(z−x)2\left( -{y}^{2}{z}^{2}+ \left( y+z \right) ^{3}x \right) \left( y-z \right) ^{2}+ \left( -{z}^{2}{x}^{2}+ \left( z+x \right) ^{3}y \right) \left( z-x \right) ^{2}+ \left( -{x}^{2}{y}^{2}+ \left( x+y \right) ^{3}z \right) \left( x-y \right) ^{2}\geq \left( 3+2\,\sqrt {2} \right) \left( x-y \right) ^{2} \left( y-z \right) ^{2} \left( z-x \right) ^{2}

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

View graph