A quartic inequality in three real variables

Proved

WorkbookSource.base_1747

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that for $x, y, z \in \mathbb{R}$ , $x^2y^2 + z^4 + x^4 + y^4 + xy^3 \geq z^2(x^2 + y^2)$ .

Source: InternLM Lean-Workbook, record lean_workbook_1747 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_1747 (x y z : ℝ) : x ^ 2 * y ^ 2 + z ^ 4 + x ^ 4 + y ^ 4 + x * y ^ 3 ≥ z ^ 2 * (x ^ 2 + y ^ 2)  :=  by sorry

Source