lean_workbook_plus_13895

Proved

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

It is $(a+b-c)^3+(a-b+c)^3+(b+c-a)^3=a^3+b^3+c^3+3(a^2b+ab^2+ac^2+a^2c+b^2c+bc^2-6abc)$ . So, $a^2b+ab^2+ac^2+a^2c+b^2c+bc^2-6abc=0\Leftrightarrow a^2b+ab^2+ac^2+a^2c+b^2c+bc^2=6abc$ . But $a^2b+a^2c+b^2c+b^2a+c^2a+c^2b\geq 6\sqrt[6]{a^6b^6c^6}=6abc$ , with equality iff $a=b=c$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13895  (a b c : ℝ) :
  (a + b - c) ^ 3 + (a - b + c) ^ 3 + (b + c - a) ^ 3 = a ^ 3 + b ^ 3 + c ^ 3 + 3 * (a ^ 2 * b + a * b ^ 2 + a * c ^ 2 + a ^ 2 * c + b ^ 2 * c + b * c ^ 2 - 6 * a * b * c)   :=  by sorry

Source

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

View graph