Prove2Me

lean_workbook_plus_38979

Proved

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

⟺9(x2+y2+z2)(x4+2y2x2+2x2z2+y4+2y2z2 \Longleftrightarrow 9(x^2 + y^2 + z^2)(x^4 + 2y^2x^2 + 2x^2z^2 + y^4 + 2y^2z^2 +z4−3yz2x−3yzx2−3y2zx)≥0 + z^4 - 3yz^2x - 3yzx^2 - 3y^2zx)\geq 0

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

View graph