Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2002P3


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.

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