Prove2Me

lean_workbook_plus_78074

Proved

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

a2+b2+(a−b)2=c2+d2+(c−d)2a^{2}+b^{2}+(a-b)^{2}=c^{2}+d^{2}+(c-d)^{2}\n ⇒2(a2−ab+b2)=2(c2−cd+d2)\Rightarrow 2(a^{2}-ab+b^{2})=2(c^{2}-cd+d^{2})\n ⇒2(a2−ab+b2)2=2(c2−cd+d2)2\Rightarrow 2(a^{2}-ab+b^{2})^{2}=2(c^{2}-cd+d^{2})^{2}\n ⇒2(a4−2a3b+3a2b2−2ab3+b4)=2(c4−2c3d+3c2d2−2cd3+d4)\Rightarrow 2(a^{4}-2a^{3}b+3a^{2}b^{2}-2ab^{3}+b^{4})=2(c^{4}-2c^{3}d+3c^{2}d^{2}-2cd^{3}+d^{4})\n ⇒a4+b4+(a−b)4=c4+d4+(c−d)4\Rightarrow a^{4}+b^{4}+(a-b)^{4}=c^{4}+d^{4}+(c-d)^{4}

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

View graph