Prove2Me

lean_workbook_plus_9739

Disproved

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

If z1=c−a−xz_1=c-a-x and z2=d−b−yz_2=d-b-y, show that (2c−2a−z1)2+(2d−2b−z2)2=z12+z22=(2a+z1)2+(2b+z2)2(2c-2a-z_1)^2+(2d-2b-z_2)^2=z_1^2+z_2^2=(2a+z_1)^2+(2b+z_2)^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9739 : ∀ c a x d b y z₁ z₂ : ℝ,  z₁ = c - a - x ∧ z₂ = d - b - y → (2 * c - 2 * a - z₁) ^ 2 + (2 * d - 2 * b - z₂) ^ 2 = z₁ ^ 2 + z₂ ^ 2 ∧ z₁ ^ 2 + z₂ ^ 2 = (2 * a + z₁) ^ 2 + (2 * b + z₂) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph