Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1990P2

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1990, Problem 2

Take n ≥ 3 and consider a set E of 2n - 1 distinct points on a circle.
Suppose that exactly k of these points are to be colored black. Such a
coloring is said to be "good" if there is at least one pair of black points
such that the interior of one of the arcs between them contains exactly n
points from E. Find the smallest value of k so that every such coloring of
k points of E is good.
-/

namespace Imo1990P2

/- determine -/ abbrev solution (n : ℕ) : ℕ := sorry

/-- Label the points by `ZMod (2 * n - 1)`. A set `B` of black points is
*good* if it contains two points `x` and `y` with `y - x = n + 1` or
`x - y = n + 1`, which is exactly the condition that one of the two arcs
between them contains `n` points of `E` in its interior. -/
def IsGood (n : ℕ) (B : Finset (ZMod (2 * n - 1))) : Prop :=
  ∃ x ∈ B, ∃ y ∈ B, y - x = ((n + 1 : ℕ) : ZMod (2 * n - 1)) ∨
    x - y = ((n + 1 : ℕ) : ZMod (2 * n - 1))

theorem imo1990_p2 (n : ℕ) (hn : 3 ≤ n) :
    IsLeast {k : ℕ | ∀ B : Finset (ZMod (2 * n - 1)), B.card = k → IsGood n B}
      (solution n) := sorry

end Imo1990P2

File author(s): Kimi K3

This problem has a complete formalized solution.