import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2010, Problem 3

Determine all functions g : ℤ>0 → ℤ>0 such that

               (g(m) + n)(g(n) + m)

is always a perfect square.
-/

namespace Imo2010P3

abbrev PosInt : Type := { x : ℤ // 0 < x }

notation "ℤ>0" => PosInt

/- determine -/ abbrev solution_set : Set (ℤ>0 → ℤ>0) := sorry


theorem imo2010_p3 (g : ℤ>0 → ℤ>0) :
    g ∈ solution_set ↔ ∀ m n, IsSquare ((g m + n) * (g n + m)) := sorry

This problem does not yet have a complete solution.