Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2014P5

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Field.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Fintype.BigOperators
public import Mathlib.Data.Rat.Star
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.FieldSimp.Lemmas
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Preprocessing
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# International Mathematical Olympiad 2014, Problem 5

For every positive integer n, the Bank of Cape Town issues coins of
denomination 1/n. Given a finite collection of such coins (of not
necessarily different denominations) with total value at most 99 + 1/2,
prove that it is possible to split this collection into 100 or fewer
groups, such that each group has total value at most 1.
-/

namespace Imo2014P5

theorem imo2014_p5 (c : Multiset ℕ) (hpos : ∀ n ∈ c, 0 < n)
    (hval : value c ≤ 99 + 1 / 2) :
    ∃ gs : Multiset (Multiset ℕ), gs.sum = c ∧ gs.card ≤ 100 ∧
      ∀ g ∈ gs, value g ≤ 1 := sorry

end Imo2014P5

File author(s): Kimi K3

This problem has a complete formalized solution.