Two cyclic cubic sums bound a cubed pairwise sum

Proved

WorkbookSource.plus_82114

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

lean-workbooksource-checked

Let $x,y,z$ be positive real numbers. Prove that $3\, \left( {x}^{2}y+{y}^{2}z+{z}^{2}x \right) \left( x{y}^{2}+y{z}^{2}+{x}^{2}z \right) \geq \left( xy+zx+yz \right) ^{3}$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_82114 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 3 * (x^2 * y + y^2 * z + z^2 * x) * (x * y^2 + y * z^2 + x^2 * z) ≥ (x * y + y * z + z * x)^3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_82114; Apache-2.0

View graph