lean_workbook_plus_75083

Proved

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

Any odd positive integer $N$ has a multiple $M$ of the form $4m^2-1$ , namely $M = N(N+2) = (N+1)^2 - 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75083 (n : ℤ) (h : n > 0 ∧ Odd n) : ∃ m : ℤ, n * (n + 2) = 4 * m ^ 2 - 1   :=  by sorry

Source