Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1978P6

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1978, Problem 6

An international society has its members from six different countries.
The list of members has 1978 names, numbered $1, 2, \ldots, 1978$.
Prove that there is at least one member whose number is
the sum of the numbers of two (not necessarily distinct) members from his own country.
-/

namespace Imo1978P6

theorem imo1978_p6 (C : Fin 1978 → Fin 6) :
  ∃ j : Fin 1978, ∃ i : Fin 1978, ∃ k : Fin 1978,
    C i = C j ∧
    C j = C k ∧
    (i:ℕ) + 1 + (k:ℕ) + 1 = (j:ℕ) + 1 := sorry


end Imo1978P6

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.