lean_workbook_plus_16379

Proved

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

$=(b-c)^2(a-c)^2+(c-a)^2(b-a)^2+(a-b)^2(c-b)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph