Prove2Me

lean_workbook_plus_65620

Proved

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

Let x= a+b+c. Show that (a+b+c)2+(3−a−b−c)2=2(x−3/2)2+9/2(a+b+c)^2+(3-a-b-c)^2= 2(x-3/2)^2+9/2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65620 (x a b c : ℝ) (h : x = a + b + c) : (a + b + c) ^ 2 + (3 - a - b - c) ^ 2 = 2 * (x - 3 / 2) ^ 2 + 9 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph