Prove2Me

lean_workbook_plus_77675

Proved

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

No need to throw complex numbers in here. Just use your stock Pythagorean triples: (x2−y2)2+(2xy)2=(x2+y2)2(x^2 - y^2)^2 + (2xy)^2 = (x^2 + y^2)^2 . \n Hence, 25(x2+y2)=(x2+y2)225(x^2 + y^2) = (x^2 + y^2)^2 and so (x2+y2)(x2+y2−25)=0(x^2 + y^2)(x^2 + y^2 - 25) = 0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77675  (x y : ℝ) :
  25 * (x^2 + y^2) = (x^2 + y^2)^2 ↔ (x^2 + y^2) * (x^2 + y^2 - 25) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph