lean_workbook_plus_29744

Disproved

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

Prove that if $p$ and $q$ are prime numbers greater than or equal to 5, then $p$ does not divide $2^q-1$ and $q$ does not divide $2^p-1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29744 : ∀ p q : ℕ, p.Prime ∧ q.Prime ∧ p >= 5 ∧ q >= 5 → ¬ (p ∣ (2^q-1)) ∧ ¬ (q ∣ (2^p-1))   :=  by sorry

Source