Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1981P6

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1981, Problem 6

Suppose that f : ℕ × ℕ → ℕ satisfies

 1) f (0, y) = y + 1
 2) f (x + 1, 0) = f (x, 1),
 3) f (x + 1, y + 1) = f (x, f (x + 1, y))

for all x y ∈ ℕ.

Determine f (4, 1981).
-/

namespace Imo1981P6

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

theorem imo1981_p6 (f : ℕ → ℕ → ℕ)
    (h1 : ∀ y, f 0 y = y + 1)
    (h2 : ∀ x, f (x + 1) 0 = f x 1)
    (h3 : ∀ x y, f (x + 1) (y + 1) = f x (f (x + 1) y)) :
    f 4 1981 = solution_value := sorry

This problem has a complete formalized solution written by David Renshaw.