lean_workbook_plus_50690

Proved

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

Prove that for $x, y, z \in \mathbb{R}$ and $u, v, w > 0$ , the following inequality holds:\n $x^2wv(v+w) + y^2uw(w+u) + z^2vu(v+u) \geq 2(xy + zx + yz)uvw$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50690 (x y z u v w : ℝ) (hu : 0 < u) (hv : 0 < v) (hw : 0 < w) : x^2 * w * v * (v + w) + y^2 * u * w * (w + u) + z^2 * v * u * (v + u) ≥ 2 * (x * y + z * x + y * z) * u * v * w   :=  by sorry

Source

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

View graph