lean_workbook_plus_25367

Disproved

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

So, it is equivalent to proving that there does not exist an integer k, such that $k^2 = mn(m^2 - n^2)$ for integers m and n such that $gcd(m,n) = 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25367 : ¬∃ (k m n : ℤ), k^2 = m*n*(m^2-n^2) ∧  Int.gcd m n = 1   :=  by sorry

Source