Prove2Me

lean_workbook_plus_66159

Open

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

Prove that for any rr, we have the algebraic identity:\n\n(ar+br−cr)(a−b)2+(br+cr−ar)(b−c)2+(cr+ar−br)(c−a)2=2[ar(a−b)(a−c)+br(b−c)(b−a)+cr(c−a)(c−b)](a^r + b^r - c^r)(a - b)^2 + (b^r + c^r - a^r)(b - c)^2 + (c^r + a^r - b^r)(c - a)^2 = 2[a^r(a - b)(a - c) + b^r(b - c)(b - a) + c^r (c - a)(c - b)]

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

View graph