lean_workbook_plus_70837

Proved

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

Prove that $(a^3+b^3+c^3+d^3)^2=9(bc-ad)(ca-bd)(ab-cd)$ for $a,b,c,d \in\mathbb{R}$ and $a+b+c+d=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70837 (a b c d : ℝ) (h : a + b + c + d = 0) :
  (a^3 + b^3 + c^3 + d^3)^2 = 9 * (b * c - a * d) * (c * a - b * d) * (a * b - c * d)   :=  by sorry

Source

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

View graph