Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1989P1

import Mathlib.Algebra.EuclideanDomain.Basic
import Mathlib.Algebra.EuclideanDomain.Int
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Finite.Card
import Mathlib.Data.Int.Star
import Mathlib.Data.Set.Card.Arithmetic
import Mathlib.Order.CompletePartialOrder
import Mathlib.Order.Interval.Finset.Fin

/-!
# 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 : ∃ (A : Fin 117 → Set ℕ),
    S = ⨆ i : Fin 117, A i ∧
    ∀ i j, i ≠ j → Disjoint (A i) (A j) ∧
    Set.ncard (A i) = 17 ∧
    ∑ᶠ a ∈ A i, a = ∑ᶠ a ∈ A j, a := sorry


end Imo1989P1

File author(s): Francesco Vercellesi

This problem has a complete formalized solution.