Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2013P2

import Mathlib

/-!
# International Mathematical Olympiad 2013, Problem 2

A configuration of 4027 points of the plane is called Colombian if it
consists of 2013 red points and 2014 blue points, and no three of the
points of the configuration are collinear. By drawing some lines, the
plane is divided into several regions. An arrangement of lines is good
for a Colombian configuration if the following two conditions are
satisfied:

 * no line passes through any point of the configuration;
 * no region contains points of both colours.

Find the least value of k such that for any Colombian configuration of
4027 points, there is a good arrangement of k lines.
-/

namespace Imo2013P2

abbrev Pt := EuclideanSpace ℝ (Fin 2)

/-- A configuration of 2013 red points and 2014 blue points in the plane,
all distinct, such that no three points of the configuration are collinear. -/
structure ColombianConfiguration where
  red : Finset Pt
  blue : Finset Pt
  red_card : red.card = 2013
  blue_card : blue.card = 2014
  red_blue_disjoint : Disjoint red blue
  not_collinear : ∀ p₁ ∈ red ∪ blue, ∀ p₂ ∈ red ∪ blue, ∀ p₃ ∈ red ∪ blue,
    p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → ¬ Collinear ℝ {p₁, p₂, p₃}

/--
An arrangement of lines (one-dimensional affine subspaces of the plane)
is *good* for a configuration if no line passes through a point of the
configuration and every red point is strictly separated from every blue
point by at least one of the lines.

(The regions determined by an arrangement of lines are convex, and two
points lying on none of the lines belong to the same region if and only
if they are strictly on the same side of every line. Therefore, requiring
each red-blue pair to be strictly separated by some line is equivalent to
requiring that no region contains points of both colours.)
-/
def GoodArrangement (cfg : ColombianConfiguration) {k : ℕ}
    (lines : Fin k → AffineSubspace ℝ Pt) : Prop :=
  (∀ i, Module.finrank ℝ (lines i).direction = 1) ∧
  (∀ i, ∀ p ∈ cfg.red ∪ cfg.blue, p ∉ lines i) ∧
  (∀ p ∈ cfg.red, ∀ q ∈ cfg.blue, ∃ i, (lines i).SOppSide p q)

/- determine -/ abbrev solution_value : ℕ := sorry

theorem imo2013_p2 :
    IsLeast {k | ∀ cfg : ColombianConfiguration,
                 ∃ lines : Fin k → AffineSubspace ℝ Pt, GoodArrangement cfg lines}
            solution_value := sorry

end Imo2013P2

File author(s): David Renshaw

This problem has a complete formalized solution.