by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that for non-negative numbers a,b,c,d,e, the following identity holds: (a+b+c+d+e)(c2+a2+b2+d2+e2)−5abc−5bcd−5cde−5ade−5abe=(e−a)2(2b+3/4d)+(d−e)2(2a+3/4c)+(c−d)2(2e+3/4b)+(b−c)2(2d+3/4a)+(a−b)2(2c+3/4e)+1/4(2c−d−e)2c+1/4(2d−e−a)2d+1/4(2e−a−b)2e+1/4(2b−c−d)2b+1/4(2a−b−c)2a.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17061 (a b c d e : ℝ) : (a+b+c+d+e)*(c^2+a^2+b^2+d^2+e^2) - 5*a*b*c - 5*b*c*d - 5*c*d*e - 5*a*d*e - 5*a*b*e = (e-a)^2*(2*b+3/4*d) + (d-e)^2*(2*a+3/4*c) + (c-d)^2*(2*e+3/4*b) + (b-c)^2*(2*d+3/4*a) + (a-b)^2*(2*c+3/4*e) + 1/4*(2*c-d-e)^2*c + 1/4*(2*d-e-a)^2*d + 1/4*(2*e-a-b)^2*e + 1/4*(2*b-c-d)^2*b + 1/4*(2*a-b-c)^2*a := by sorry