Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1991P2

import Mathlib

/-!
# International Mathematical Olympiad 1991, Problem 2

Let n > 6 be an integer and a₁, a₂, ..., aₖ be all the
natural numbers less than n and relatively prime to n.
If

  a₂ - a₁ = a₃ - a₂ = ... = aₖ - aₖ₋₁ > 0,

prove that n must either be a prime number of a power
of 2.
-/

namespace Imo1991P2

theorem imo1991_p2 (n : ℕ) (hn : 6 < n)
    (k : ℕ) (a : Fin k → ℕ)
    (ha1 : { a i | i } = { m | Nat.Coprime m n ∧ m < n })
    (d : ℕ) (hd : 0 < d)
    (ha2 : ∀ i : Fin k, (h : i + 1 < k) → a i + d = a ⟨i + 1, h⟩) :
    n.Prime ∨ n.isPowerOfTwo := sorry

end Imo1991P2

This problem does not yet have a complete formalized solution.