lean_workbook_plus_5481

Proved

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

When $a > 0$ , rewrite the equation $a^2+b^2+(ab)^2=c^2$ as a classical Pell-Fermat equation $x^2-ny^2=m$ with $n = a^2+1$ , $m = a^2$ , and $(b,c) = (y,x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5481  (a b c x y : ℤ) (n m : ℤ) (h₁ : a > 0) (h₂ : n = a^2 + 1) (h₃ : m = a^2) (h₄ : (b, c) = (y, x)) : a^2 + b^2 + (a * b)^2 = c^2 ↔ x^2 - n * y^2 = m   :=  by sorry

Source

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

View graph