Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1998P6

import Mathlib

/-!
# International Mathematical Olympiad 1998, Problem 6

Determine the least possible value of `f(1998)`, where `f : ℕ+ → ℕ+` satisfies
`f(n^2 * f(m)) = m * f(n)^2` for all `m, n ∈ ℕ+`.
-/

namespace Imo1998P6

/- determine -/ abbrev answer : ℕ+ := sorry

theorem imo1998_p6 :
    IsLeast
      {k : ℕ+ | ∃ f : ℕ+ → ℕ+, (∀ m n : ℕ+, f (n ^ 2 * f m) = m * f n ^ 2) ∧ f 1998 = k}
      answer := sorry

end Imo1998P6

File author(s): Daniel Liao

This problem has a complete formalized solution.