Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2007P3

module

public import Mathlib.Combinatorics.SimpleGraph.Clique

public section


/-!
# International Mathematical Olympiad 2007, Problem 3

In a mathematical competition some competitors are (mutual) friends.
Call a group of competitors a clique if each two of them are friends.
Given that the largest size of a clique is even, prove that the
competitors can be arranged into two rooms such that the largest size
of a clique contained in one room is the same as the largest size of
a clique contained in the other room.
-/

namespace Imo2007P3

/-- The largest size of a clique of the graph `G` all of whose vertices lie in `A`. -/
noncomputable def maxCliqueCard {V : Type*} (G : SimpleGraph V) (A : Finset V) : ℕ :=
  sSup {n : ℕ | ∃ s : Finset V, s ⊆ A ∧ G.IsClique s ∧ s.card = n}

theorem imo2007_p3 {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    (hG : Even (maxCliqueCard G Finset.univ)) :
    ∃ A B : Finset V, Disjoint A B ∧ A ∪ B = Finset.univ ∧
      maxCliqueCard G A = maxCliqueCard G B := sorry

end Imo2007P3

File author(s): Kimi K3

This problem has a complete formalized solution.