lean_workbook_plus_56363

Proved

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

Prove the inequality $(x^2+2y^2-xy)z^2+(x^3-xy^2-4x^2y)z+yx^3+y^2x^2\geq 0$ for $x, y, z > 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56363 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x^2 + 2*y^2 - x*y) * z^2 + (x^3 - x*y^2 - 4*x^2*y) * z + y*x^3 + y^2*x^2 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph