Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1997P5

import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.Tactic.IntervalCases

/-!
# International Mathematical Olympiad 1997, Problem 5

Determine all pairs of integers 1 ≤ a,b that satisfy a ^ (b ^ 2) = b ^ a.
-/

namespace Imo1997P5

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

theorem imo1997_p5 (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    a ^ (b ^ 2) = b ^ a ↔ (a, b) ∈ solution_set := sorry

end Imo1997P5

File author(s): Roozbeh Yousefzadeh, Ilmārs Cīrulis

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/imo_proofs/imo_1997_p5.lean.