import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.ModEq import Mathlib.Algebra.GroupPower.Basic import Mathlib.Tactic /-! # International Mathematical Olympiad 1964, Problem 1 (a) Find all natural numbers n for which 2ⁿ - 1 is divisible by 7. (b) Prove that there is no positive integer n for which 2ⁿ + 1 is divisible by 7. -/ namespace Imo1964P1 /- determine -/ abbrev solution_set : Set ℕ := sorry theorem imo_1964_p1a (n : ℕ) : n ∈ solution_set ↔ 2^n ≡ 1 [MOD 7] := sorry theorem imo_1964_p1b (n : ℕ) : ¬ 7 ∣ (2^n + 1) := sorry

This problem has a complete solution written by David Renshaw and Anand Rao.