Prove2Me

lean_workbook_plus_29806

Proved

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

We really just care if it divisible by 3 or not. We want 2n≡1 (mod 3)2^n\equiv1\, (\textrm{mod 3}) .\n\n 21≡2 (mod 3)2^1\equiv2\,(\textrm{mod 3}) \n 22≡1 (mod 3)2^2\equiv1\,(\textrm{mod 3}) \n 23≡2 (mod 3)2^3\equiv2\,(\textrm{mod 3}) \nBecause it keeps repeating, you see that 2n−1≡0 (mod 3)2^n-1\equiv0\,(\textrm{mod 3}) is true for all positive even nn

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29806  (n : ℕ)
  (h₀ : Even n) :
  3 ∣ (2^n - 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph