Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1999P4

import Mathlib
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1999, Problem 4

Determine all pairs of positive integers (n,p) such that p is
a prime, n not exceeded 2p, and (p-1)ⁿ + 1 is divisible by of nᵖ⁻¹.
-/

namespace Imo1999P4

/- determine -/ abbrev SolutionSet : Set (ℕ × ℕ) := sorry

theorem imo1999_p4 (n p : ℕ) :
    (n,p) ∈ SolutionSet ↔
    0 < n ∧ n ≤ 2 * p ∧ p.Prime ∧ n^(p - 1) ∣ (p - 1)^n + 1 := sorry

end Imo1999P4

File author(s): Benpigchu

This problem has a complete formalized solution.