Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2002P3

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 imo2002_p3 {m n : ℕ} (hm : 3 ≤ m) (hn : 3 ≤ n) :
    ⟨m, n⟩ ∈ solution ↔
    {a : ℤ | 0 < a ∧ a ^ n + a ^ 2 - 1 ∣ a ^ m + a - 1}.Infinite := sorry

end Imo2002P3

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2002Q3.lean.