lean_workbook_plus_8999

Proved

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

Let $m$ be a positive odd integer, $m > 2.$ Find the smallest positive integer $n$ such that $2^{1989}$ divides $m^n - 1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8999 (m : ℕ) (hm1 : 2 < m) (hm2 : Odd m) : ∃ n : ℕ, (2^1989 ∣ m^n - 1) ∧ (∀ k : ℕ, (2^1989 ∣ m^k - 1) → n ≤ k)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph