Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1992P3

module

public import Mathlib.Tactic
public import Mathlib.Data.Finset.Sym

public section


/-!
# International Mathematical Olympiad 1992, Problem 3

Consider 9 points in space, no 4 coplanar. Each pair of points is joined by a
line segment which is colored either blue or red or left uncolored. Find the
smallest value of n such that whenever exactly n edges are colored, the set of
colored edges necessarily contains a triangle all of whose edges have the same
color.
-/

namespace Imo1992P3

/-- An edge coloring of the complete graph on 9 vertices by two colors
(encoded as `Fin 2`), where some edges may be left uncolored (`none`).
The vertices are indexed by `Fin 9` and the edges by unordered pairs
`Sym2 (Fin 9)`; the geometric hypotheses of the problem (9 points in space,
no 4 of them coplanar) only serve to guarantee that every pair of points
determines an edge, so the problem is purely combinatorial. -/
structure EdgeColoring where
  /-- the color assigned to the edge joining two vertices -/
  color : Sym2 (Fin 9) → Option (Fin 2)
  /-- there is no edge from a vertex to itself -/
  diag : ∀ i : Fin 9, color s(i, i) = none

/-- The colored edges of an edge coloring, represented as the set of edges
that received a color. (Diagonal "edges" `s(i, i)` are never colored, so this
is exactly the set of colored segments joining two distinct points.) -/
def EdgeColoring.coloredEdges (c : EdgeColoring) : Finset (Sym2 (Fin 9)) :=
  Finset.filter (fun e => (c.color e).isSome) Finset.univ

/-- The uncolored edges of an edge coloring, represented as the set of
non-diagonal edges that were left uncolored. -/
def EdgeColoring.uncoloredEdges (c : EdgeColoring) : Finset (Sym2 (Fin 9)) :=
  Finset.filter (fun e => c.color e = none ∧ ¬ e.IsDiag) Finset.univ

/-- A coloring has a monochromatic triangle if there are three distinct
vertices whose three connecting edges all have the same color. -/
def EdgeColoring.HasMonoTriangle (c : EdgeColoring) : Prop :=
  ∃ i j k : Fin 9, i ≠ j ∧ j ≠ k ∧ k ≠ i ∧
    ∃ b : Fin 2, c.color s(i, j) = some b ∧ c.color s(j, k) = some b ∧
      c.color s(k, i) = some b

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

theorem imo1992_p3 :
    IsLeast {n : ℕ | ∀ c : EdgeColoring, c.coloredEdges.card = n →
      c.HasMonoTriangle} answer := sorry

end Imo1992P3

File author(s): Kimi K3

This problem has a complete formalized solution.