import public import Mathlib
/-!
# International Mathematical Olympiad 2002, Problem 3
Find all pairs of positive integers m,n ≥ 3 for which
there exist infinitely many positive integers a such that
(aᵐ + a - 1) / (aⁿ + a² - 1)
is itself an integer.
-/
namespace Imo2002P3
/- determine -/ abbrev solution : Set (ℕ × ℕ) := sorry
theorem imo2002P3 (m n : ℕ) :
⟨m, n⟩ ∈ solution ↔
Set.Infinite { a : ℤ | 0 < a ∧ a ^ n + a ^ 2 - 1 ∣ a ^ m + a - 1 } := sorry
end Imo2002P3
This problem does not yet have a complete formalized solution.