Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2010P3

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 SolutionSet : Set (ℤ>0 → ℤ>0) := sorry

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


end Imo2010P3

This problem does not yet have a complete formalized solution.