Prove2Me

lean_workbook_plus_12622

Proved

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

Now 12∑a2(b−c)2=\dfrac {1}{2}\sum a^2(b-c)^2 = 12((2/2)2(−2/2−0)2+(−2/2)2(0−2/2)2)= \dfrac {1}{2}\Big ((\sqrt{2}/2)^2(-\sqrt{2}/2 - 0)^2 + (-\sqrt{2}/2)^2(0-\sqrt{2}/2)^2 \Big) = 12(1/4+1/4)=1/4 \dfrac {1}{2}(1/4+1/4) = 1/4 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12622 :
  1 / 2 * ((Real.sqrt 2 / 2)^2 * (-(Real.sqrt 2 / 2) - 0)^2 + (-(Real.sqrt 2 / 2))^2 * (0 - (Real.sqrt 2 / 2))^2) = 1 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph