lean_workbook_plus_5314

Proved

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

Let $k\in \mathbb{Z^+},$ $m$ is an odd natural number. Prove that exists $n\in \mathbb{Z^+}$ such that $2^k\mid n^n-m$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5314 (k m : ℕ) (hm : Odd m) : ∃ n : ℕ, 2 ^ k ∣ n ^ n - m   :=  by sorry

Source