Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1978P3

import Mathlib

/-!
# International Mathematical Olympiad 1978, Problem 3

The set of all positive integers is the union of two disjoint subsets
{f(1), f(2), ..., f(n), ...} and {g(1), g(2), ..., g(n), ...}, where

  f(1) < f(2) < ... < f(n) < ...,
  g(1) < g(2) < ... < g(n) < ...,

and g(n) = f(f(n)) + 1 for all n ≥ 1.

Determine f(240).
-/

namespace Imo1978P3

/- determine -/ abbrev solution : ℕ := sorry

theorem imo1978_p3
    (f g : ℕ → ℕ)
    (hfpos : ∀ n, 0 < n → 0 < f n)
    (hgpos : ∀ n, 0 < n → 0 < g n)
    (hfmono : ∀ n m, 0 < n → n < m → f n < f m)
    (hgmono : ∀ n m, 0 < n → n < m → g n < g m)
    (hdisjoint : ∀ n m, 0 < n → 0 < m → f n ≠ g m)
    (hcover : ∀ k, 0 < k → (∃ n, 0 < n ∧ f n = k) ∨ (∃ n, 0 < n ∧ g n = k))
    (hgf : ∀ n, 0 < n → g n = f (f n) + 1) :
    f 240 = solution := sorry

end Imo1978P3

File author(s): David Renshaw

This problem has a complete formalized solution.