Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1999P4


import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1999, Problem 4

Determine all pairs of positive integers (x,p) such that p is
a prime and xᵖ⁻¹ is a divisor of (p-1)ˣ + 1.
-/

namespace Imo1999P4

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

theorem imo1999_p4 (x p : ℕ) :
    ⟨x,p⟩ ∈ SolutionSet ↔
    0 < x ∧ p.Prime ∧ x^(p - 1) ∣ (p - 1)^x + 1 := sorry

This problem does not yet have a complete formalized solution.

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