Prove2Me

A three-factor sum-of-two-squares identity

Proved
WorkbookSource.problem_7972

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

lean-workbooksource-checked

Prove that (a2+x2)(b2+y2)(c2+z2)=(ayz+bxz+cxy−abc)2+(xbc+yac+zab−xyz)2(a^{2}+x^{2})(b^{2}+y^{2})(c^{2}+z^{2})=(ayz+bxz+cxy-abc)^2+(xbc+yac+zab-xyz)^2 where a,b,c,x,y,za, b, c, x, y, z are non-negative numbers.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_7972 (a b c x y z: ℝ) : (a ^ 2 + x ^ 2) * (b ^ 2 + y ^ 2) * (c ^ 2 + z ^ 2) = (a * y * z + b * x * z + c * x * y - a * b * c) ^ 2 + (x * b * c + y * a * c + z * a * b - x * y * z) ^ 2  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_7972; Apache-2.0

View graph