Prove2Me

lean_workbook_plus_82174

Proved

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

proofwiki

Expand and simplify (b−a2)2+(c−a2)2+(d−a2)2+(e−a2)2(b - \frac {a}{2})^2 + (c - \frac {a}{2})^2 + (d - \frac {a}{2})^2 + (e - \frac {a}{2})^2

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

View graph