Prove2Me

lean_workbook_plus_2143

Proved

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

Prove that 4(a2−ab+b2)(b2−bc+c2)(c2−ca+a2)−((a+b)(b+c)(c+a)−6abc)2=3(a−b)2(b−c)2(c−a)24(a^2 - ab + b^2)(b^2 - bc + c^2)(c^2 - ca + a^2) - \left((a + b)(b + c)(c + a) - 6abc\right)^2 = 3(a - b)^2(b - c)^2(c - a)^2

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

View graph