lean_workbook_plus_19006

Proved

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

Suppose that a,b,c are complex numbers such that $a+b+c=0$ . Prove that $2(a-b)^2(b-c)^2(c-a)^2=(a^2+b^2+c^2)^3-54a^2b^2c^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19006 (a b c : ℂ) (h : a + b + c = 0) :
  2 * (a - b) ^ 2 * (b - c) ^ 2 * (c - a) ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2) ^ 3 - 54 * a ^ 2 * b ^ 2 * c ^ 2   :=  by sorry

Source

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

View graph