Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2020P3

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Nat
public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Nat.SuccPred
public import Mathlib.Tactic.Ring

public section


/-!
# International Mathematical Olympiad 2020, Problem 3

There are 4n pebbles of weights 1,2,3,...,4n. Each pebble is colored
in one of n colors and there are four pebbles of each color. Show
that we can arrange the pebbles into two piles such that the total
weights of both piles are the same, and each pile contains two
pebbles of each color.
-/

namespace Imo2020P3

open scoped Finset

theorem imo2020_p3 {n : ℕ} {c : Fin (4 * n) → Fin n} (h : ∀ i, #{j | c j = i} = 4) :
    ∃ S : Finset (Fin (4 * n)), ∑ i ∈ S, ((i : ℕ) + 1) = ∑ i ∈ Sᶜ, ((i : ℕ) + 1) ∧
      ∀ i, #{j ∈ S | c j = i} = 2 := sorry

end Imo2020P3

File author(s): Joseph Myers, Kimi K3

This problem has a complete formalized solution.