## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1964P1

```
import Mathlib.Data.Nat.ModEq
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
end Imo1964P1
```

File author(s): David Renshaw, Anand Rao

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: