Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1989P1

import Mathlib

/-!
# International Mathematical Olympiad 1989, Problem 1

Prove that the integers from 1 to 1989 can be partitioned in 117 sets
of 17 elements each, all with the same sum of elements.
-/

namespace Imo1989P1

abbrev S := Finset.Icc 1 1989

theorem imo1989_p1 : ∃ (P : Finpartition S),
    P.parts.card = 117 ∧
    (∀ p ∈ P.parts, p.card = 17) ∧
    (∀ p ∈ P.parts, ∀ q ∈ P.parts, p.sum id = q.sum id) := sorry

end Imo1989P1

File author(s): Francesco Vercellesi

This problem has a complete formalized solution.