lean_workbook_plus_7580

Proved

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

Let $a,b,c,d\geq 0$ ,prove that: \n\n $(a+b)(b+c)(c+d)(d+a)(c+a)(b+d)-\frac{2}{3}(a+b+c+d)(ab+bc+cd+ad+ac+bd)(acd+abd+abc+bcd)$ $=1/6\, \left( ab-cd \right) ^{2}bd+1/6\, \left( bc-ad \right) ^{2}ac+1/6\, \left( ad-bc \right) ^{2}ac+1/3\, \left( bd-ac \right) ^{2}bc+1/3\, \left( ac-bd \right) ^{2}ab+1/3\, \left( bd-ac \right) ^{2}ad+1/3\, \left( ac-bd \right) ^{2}cd+1/6\, \left( cd-ab \right) ^{2}bd+ \left( ad-bc \right) ^{2} \left( 1/6\,bd+1/3\,cd \right) + \left( ab-cd \right) ^{2} \left( 1/6\,ac+1/3\,ad \right) + \left( bc-ad \right) ^{2} \left( 1/6\,bd+1/3\,ab \right) + \left( cd-ab \right) ^{2} \left( 1/6\,ac+1/3\,bc \right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7580  (a b c d : ℝ) :
  (a + b) * (b + c) * (c + d) * (d + a) * (c + a) * (b + d) - (2 / 3) * (a + b + c + d) * (a * b + b * c + c * d + d * a + a * c + b * d) * (a * c * d + a * b * d + a * b * c + b * c * d) =
  (1 / 6) * (a * b - c * d) ^ 2 * b * d + (1 / 6) * (b * c - a * d) ^ 2 * a * c + (1 / 6) * (a * d - b * c) ^ 2 * a * c + (1 / 3) * (b * d - a * c) ^ 2 * b * c + (1 / 3) * (a * c - b * d) ^ 2 * a * b + (1 / 3) * (b * d - a * c) ^ 2 * a * d + (1 / 3) * (a * c - b * d) ^ 2 * c * d + (1 / 6) * (c * d - a * b) ^ 2 * b * d + (a * d - b * c) ^ 2 * (b * d / 6 + c * d / 3) + (a * b - c * d) ^ 2 * (a * c / 6 + a * d / 3) + (b * c - a * d) ^ 2 * (b * d / 6 + a * b / 3) + (c * d - a * b) ^ 2 * (a * c / 6 + b * c / 3)   :=  by sorry

Source

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

View graph