lean_workbook_plus_36478

Disproved

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

Show that $2018(m + 2^k)^2 + 20182017(m + 2^k) + 2017$ is divisible by $2^{k+1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36478 : ∀ m k : ℕ, (2018 * (m + 2 ^ k) ^ 2 + 20182017 * (m + 2 ^ k) + 2017) % (2 ^ (k + 1)) = 0   :=  by sorry

Source