lean_workbook_plus_36586

Proved

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

Given the formulas: $X=(t^2+4kt-8k^2)p^2+2(2k-t)ps-s^2$ , $Y=(3t^2-12kt+8k^2)p^2-2(2k-t)ps+s^2$ , $Z=2(2k-t)^2p^2-2(2k-t)ps$ , $W=t^2p^2+2(2k-t)ps-s^2$ , find the values of $p,s,t,k$ that satisfy the equation $X^2+Y^2=2Z^2+2W^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36586 (X Y Z W : ℤ) (p s t k : ℤ) (h₁ : X = (t^2 + 4 * k * t - 8 * k^2) * p^2 + 2 * (2 * k - t) * p * s - s^2) (h₂ : Y = (3 * t^2 - 12 * k * t + 8 * k^2) * p^2 - 2 * (2 * k - t) * p * s + s^2) (h₃ : Z = 2 * (2 * k - t)^2 * p^2 - 2 * (2 * k - t) * p * s) (h₄ : W = t^2 * p^2 + 2 * (2 * k - t) * p * s - s^2) : X^2 + Y^2 = 2 * Z^2 + 2 * W^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph