Prove2Me

lean_workbook_plus_33541

Proved

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

Let A=u+v,B=u−vA=u+v,B=u-v . Notice that 2p−u−v=2p−A2p-u-v=2p-A . \nThe given expression is equivalent to 2p2=u2+v2⇒2p2=A2+B22⇒4p2=A2+B22p^{2}=u^{2}+v^{2}\Rightarrow 2p^{2}=\frac{A^{2}+B^{2}}{2}\Rightarrow 4p^{2}=A^{2}+B^{2} \nThis gives us: 4p2−A2=B2⇒(2p−A)(2p+A)=B24p^{2}-A^{2}=B^{2}\Rightarrow (2p-A)(2p+A)=B^{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33541  (u v p a b : ℂ)
  (h₀ : a = u + v)
  (h₁ : b = u - v)
  (h₂ : 2 * p - u - v = 2 * p - a)
  (h₃ : 2 * p ^ 2 = u^2 + v^2) :
  (2 * p - a) * (2 * p + a) = b^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph