lean_workbook_plus_16524

Proved

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

Let $a = x+y , b = x+z , c = y+z$ , where $x,y,z > 0$ : \n\n $(x+y)^3+(x+z)^3+(y+z)^3+8xyz \ge 4(x+y)(x+z)(y+z) \ \ \iff \ \ 2(x^3+y^3+z^3) \ge x^2(y+z)+y^2(x+z)+z^2(x+y)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph