Prove2Me

lean_workbook_plus_54784

Proved

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

Suppose yy between xx and z.z. By AM-GM Inequality, we have \n 4 xyz(xy+zx+yz)(x+y+z)⩽[zx(x+y+z)+y(xy+yz+zx)]2.4\,xyz \left( xy+zx+yz \right) \left( x+y+z \right) \leqslant [zx(x+y+z)+y(xy+yz+zx)]^2. We need to prove that \n 3 xyz+x2y+y2z+z2x⩾xy(x+y+z)+z(xy+yz+zx),3\,xyz+{x}^{2}y+{y}^{2}z+{z}^{2}x \geqslant xy(x+y+z)+z(xy+yz+zx), equivalent to \n x(x−y)(y−z)⩾0.x(x-y)(y-z) \geqslant 0. Which is true.\n

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54784  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z)
  (h₁ : y ≠ x)
  (h₂ : y ≠ z)
  (h₃ : z ≠ x)
  (h₄ : x + y + z = 1) :
  4 * x * y * z * (x * y + y * z + z * x) * (x + y + z) ≤ (z * x * (x + y + z) + y * (x * y + y * z + z * x))^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph