Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1993P5

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1993, Problem 5

Let ℕ+ be the set of positive integers. Determine whether
there exists a function f : ℕ+ → ℕ+ such that
  i) f(1) = 2
  ii) f(f(n)) = f(n) + n for all n
  iii) f(n + 1) > f(n) for all n.
-/

namespace Imo1993P5

/- determine -/ abbrev DoesExist : Bool := sorry

abbrev Good (f : ℕ+ → ℕ+) : Prop := f 1 = 2 ∧ ∀ n, f (f n) = f n + n ∧ ∀ n, f n < f (n + 1)

theorem imo1993_p5 :
    if DoesExist then ∃ f, Good f else ¬∃ f, Good f := sorry


end Imo1993P5

File author(s): Zheng Yuan

This problem does not yet have a complete formalized solution.