lean_workbook_plus_6682
Disprovedor
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6682 : ∀ x y z : ℝ, 2 * (x ^ 3 + y ^ 3 + z ^ 3) ≥ x ^ 2 * (y + z) + y ^ 2 * (z + x) + z ^ 2 * (x + y) := by sorry
Source
or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6682 : ∀ x y z : ℝ, 2 * (x ^ 3 + y ^ 3 + z ^ 3) ≥ x ^ 2 * (y + z) + y ^ 2 * (z + x) + z ^ 2 * (x + y) := by sorry