lean_workbook_plus_18331

Proved

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

We have that $2(a^{2}+b^{2}+c^{2})(a+b+c)=3(ab+bc+ca)(a+b+c)$ or equivalently and then Schur\n $2(a^{3}+b^{3}+c^{3})=ab(a+b)+bc(b+c)+ca(c+a)+9abc\leq a^{3}+b^{3}+c^{3}+12abc$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18331  (a b c : ℝ) :
  2 * (a^2 + b^2 + c^2) * (a + b + c) = 3 * (a * b + b * c + c * a) * (a + b + c) ↔
  2 * (a^3 + b^3 + c^3) = a * b * (a + b) + b * c * (b + c) + c * a * (c + a) + 9 * a * b * c   :=  by sorry

Source

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

View graph