Prove2Me

lean_workbook_plus_77667

Proved

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

Prove the inequality x4+y4+z4−x3y−x3z−y3z−y3x−z3x−z3y+xyz2+xy2z+x2yz≥0x^4+y^4+z^4-x^3y-x^3z-y^3z-y^3x-z^3x-z^3y+xyz^2+xy^2z+x^2yz \ge 0.

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

View graph