Prove2Me

Simplifying a quadratic constraint

Proved
WorkbookSource.problem_34929

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

lean-workbooksource-checked

Let x,y,zx,y,z be real numbers satisfying

(x+y)2+(y+z)2+(z+x)2+4(x2+yz+xz+yx)=128.(x+y)^2+(y+z)^2+(z+x)^2+4(x^2+yz+xz+yx)=128.

Then

x2+y2+z2+3(xy+xz+yz)=64−2x2.x^2+y^2+z^2+3(xy+xz+yz)=64-2x^2.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_34929 (x y z : ℝ) : (x + y) ^ 2 + (y + z) ^ 2 + (z + x) ^ 2 + 4 * (x ^ 2 + y * z + x * z + y * x) = 128 → x ^ 2 + y ^ 2 + z ^ 2 + 3 * (x * y + x * z + y * z) = 64 - 2 * x ^ 2  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_34929; Apache-2.0

View graph