Prove2Me

lean_workbook_plus_5559

Proved

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

Identity for a,b,c a,b,c (even if a+b+c≠1 a+b+c\ne1 ): 10(a3+b3+c3)(a+b+c)2−9(a5+b5+c5)=(a+b+c)5+152(a+b)(a+c)(b+c)((a−b)2+(a−c)2+(b−c)2) {10 \left( {a}^{3}+{b}^{3}+{c}^{3} \right) \left( a+b+c \right) ^{2} -9\left({a}^{5}+{b}^{5}+{c}^{5}\right)= \left( a+b+c \right) ^{5}+\frac{15}{2} \left( a+b \right) \left( a+c \right) \left( b+c \right) \left( \left( a-b \right) ^{2}+ \left( a-c \right) ^{2}+ \left( b-c \right) ^{2} \right)}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5559 (a b c : ℝ) :
  10 * (a^3 + b^3 + c^3) * (a + b + c)^2 - 9 * (a^5 + b^5 + c^5) =
    (a + b + c)^5 + (15 / 2) * (a + b) * (a + c) * (b + c) * ((a - b)^2 + (a - c)^2 + (b - c)^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph