Prove2Me

lean_workbook_plus_79951

Proved

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

(a+b+c+d)2−8(ac+bd)=(a+b−c−d)2−4(a−b)(c−d)(a+b+c+d)^2-8(ac+bd)=(a+b-c-d)^2-4(a-b)(c-d)

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

View graph