Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2019P1

import Mathlib.Data.PNat.Basic
import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2019, Problem 1

Let ℕ+ be the set of positive integers.
A function f: ℕ+ → ℕ+ satisfies the equation

  fᶠ⁽ⁿ⁾(n)⬝f²(n) = n^2

for all positive integers n, where fᵏ(m) means f iterated k times on m.
Given this information, determine all possible values of f(1000).
-/

namespace Usa2019P1

/- determine -/ abbrev solution_set : Set ℕ+ := sorry

theorem usa2019_p1 (m : ℕ+) :
   m ∈ solution_set ↔
    (∃ f : ℕ+ → ℕ+,
      (∀ n, f^[f n] n * f (f n) = n ^ 2) ∧
      m = f 1000) := sorry


end Usa2019P1

File author(s): David Renshaw

This problem has a complete formalized solution.