lean_workbook_plus_23287

Disproved

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

Prove that for even values of positive n, $2^n-1$ is congruent to $1 \pmod 3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23287 : ∀ n : ℕ, Even n ∧ n > 0 → (2^n - 1 ≡ 1 [ZMOD 3])   :=  by sorry

Source