Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1993P5

import Mathlib.Data.Real.GoldenRatio
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1993, Problem 5

Does there exist 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): Roozbeh Yousefzadeh, Zheng Yuan

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/Lean_v20/imo_proofs/imo_1993_p5.lean.