lean_workbook_plus_53179
ProvedFirst, we know is a solution. We can construct infinite solution as follows: Assume that is a solution.(So ) We can take positive integer such that . Set ( ). Then, you can easily confirm and is a perfect square. You are done. (example: (x,y)=(113, 84), (262621633, 151245528))
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53179 (m n : ℕ) (h₁ : Nat.gcd m 2*n = 1) (h₂ : ∃ k : ℕ, m^4 - 2*n^4 = k^2) : ∃ x y : ℕ, Nat.gcd x 2*y = 1 ∧ ∃ k : ℕ, x^4 - 2*y^4 = k^2 := by sorry
Source