Prove2Me

lean_workbook_plus_75775

Proved

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

prove that: x4y2+y4z2+z4x2≥14(yz(x2+yz)(y2+xz)+zx(y2+xz)(z2+xy)+xy(z2+xy)(x2+yz))x^4y^2+y^4z^2+z^4x^2 \geq \frac{1}{4}(yz(x^2+yz)(y^2+xz)+zx(y^2+xz)(z^2+xy)+xy(z^2+xy)(x^2+yz))

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

View graph