lean_workbook_plus_12643

Proved

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

Show that there are infinitely many integer solutions $(m,n)$ for the equation $(m+1)(n-1) = (m-n+1)(m-n-1).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12643 (m n : ℤ) : ∃ m n, (m+1)*(n-1) = (m-n+1)*(m-n-1)   :=  by sorry

Source