Prove2Me

lean_workbook_plus_74575

Proved

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

Given a,b,c≥0a, b, c \geq 0, prove the following identity for degree 3:\n(a+b+c4)∑a(a−b)(a−c)=bc(b−c)2+ca(c−a)2+ab(a−b)24+(2a2−b2−c2−ab+2bc−ca)24(a + \frac{b + c}{4}) \sum a(a - b)(a - c) = bc(b - c)^2 + \frac{ca(c - a)^2 + ab(a - b)^2}{4} + \frac{(2a^2 - b^2 - c^2 - ab + 2bc - ca)^2}{4}

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

View graph