Prove2Me

A five-variable quadratic decomposition

Proved
WorkbookSource.problem_27766

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Given the identity (a+b+c+d+e)2−52(a(b+c)+b(c+d)+c(d+e)+d(e+a)+e(a+b))=116(4e−d−c−b−a)2+15144(3d−c−b−a)2+524(2c−b−a)2+58(b−a)2(a+b+c+d+e)^2 - \frac{5}{2}(a(b+c)+b(c+d)+c(d+e)+d(e+a)+e(a+b)) = \frac{1}{16}(4e-d-c-b-a)^2 + \frac{15}{144}(3d-c-b-a)^2 + \frac{5}{24}(2c-b-a)^2 + \frac{5}{8}(b-a)^2

Source: InternLM Lean-Workbook, record lean_workbook_27766 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_27766 (a b c d e : ℝ) : (a + b + c + d + e) ^ 2 - (5 / 2) * (a * (b + c) + b * (c + d) + c * (d + e) + d * (e + a) + e * (a + b))  = (1 / 16) * (4 * e - d - c - b - a) ^ 2 + (15 / 144) * (3 * d - c - b - a) ^ 2 + (5 / 24) * (2 * c - b - a) ^ 2 + (5 / 8) * (b - a) ^ 2  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_27766; Apache-2.0

View graph