lean_workbook_plus_690

Proved

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

Prove that for $x, y, z >0$ , $x^3y+y^3z+z^3x+xy^3+yz^3+zx^3\geq 2(x^2y^2+y^2z^2+z^2x^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_690 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) : x^3*y + y^3*z + z^3*x + x*y^3 + y*z^3 + z*x^3 >= 2 * (x^2*y^2 + y^2*z^2 + z^2*x^2)   :=  by sorry

Source

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

View graph