Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1978P6

import Mathlib

/-!
# 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 : Finset.Icc 1 1978 → Fin 6) :
  ∃ j i k, C i = C j ∧ C j = C k ∧ i.val + k.val = j.val := sorry

end Imo1978P6

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

This problem has a complete formalized solution.