lean_workbook_plus_42485

Disproved

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

Given $m > n$ and $gcd(2^n, 2^n - 1) = 1$ , prove that $2^n - 1$ divides $2^{m-n} + 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42485 : ∀ m n : ℕ, m > n ∧ Nat.gcd (2 ^ n) (2 ^ n - 1) = 1 → (2 ^ n - 1) ∣ (2 ^ (m - n) + 1)   :=  by sorry

Source