lean_workbook_plus_8780

Proved

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

Prove that for $x = a + b; y = b + c; z = c + a$ and $a, b, c > 0$ , $a^3 +b^3 +c^3 +a^2 b +b^2 c+c^2 a \geq 2(ab^2 +bc^2 +ca^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8780 (x y z a b c : ℝ) (hx : x = a + b) (hy : y = b + c) (hz : z = c + a) (hab : a > 0 ∧ b > 0 ∧ c > 0) : a^3 + b^3 + c^3 + a^2 * b + b^2 * c + c^2 * a >= 2 * (a * b^2 + b * c^2 + c * a^2)   :=  by sorry

Source

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

View graph