Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2019P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.SimpleGraph.Girth

public section


/-!
# International Mathematical Olympiad 2019, Problem 3

A social network has 2019 users, some pairs of which are friends (friendship is
symmetric). If A, B, C are three users such that AB are friends and AC are friends
but BC is not, then the administrator may perform the following operation: change
the friendships such that BC are friends, but AB and AC are no longer friends.
Initially, 1009 users have 1010 friends and 1010 users have 1009 friends. Prove
that the administrator can make a sequence of operations such that all users have
at most 1 friend.
-/

namespace Imo2019P3

open SimpleGraph Finset

attribute [local instance] Classical.propDecidable

attribute [-instance] SimpleGraph.Sup.adjDecidable SimpleGraph.Inf.adjDecidable
  SimpleGraph.Sdiff.adjDecidable SimpleGraph.Bot.adjDecidable
  SimpleGraph.Top.adjDecidable SimpleGraph.Compl.adjDecidable
  SimpleGraph.fintypeEdgeSetSup SimpleGraph.fintypeEdgeSetInf
  SimpleGraph.fintypeEdgeSetSdiff SimpleGraph.fintypeEdgeSetBot

/-- The operation of the problem: if `a` is friends with both `b` and `c`, but `b` and
`c` are not friends, then the friendships `ab` and `ac` are deleted and the friendship
`bc` is created.  `Toggle G G'` says that `G'` is obtained from `G` by one such
operation. -/
def Toggle {V : Type*} (G G' : SimpleGraph V) : Prop :=
  ∃ a b c : V, b ≠ c ∧ G.Adj a b ∧ G.Adj a c ∧ ¬ G.Adj b c ∧
    G' = (G.deleteEdges {s(a, b), s(a, c)}) ⊔ fromEdgeSet {s(b, c)}

theorem imo2019_p3 (G : SimpleGraph (Fin 2019))
    (h1009 : (Finset.univ.filter (fun v => G.degree v = 1009)).card = 1010)
    (h1010 : (Finset.univ.filter (fun v => G.degree v = 1010)).card = 1009) :
    ∃ G' : SimpleGraph (Fin 2019), Relation.ReflTransGen Toggle G G' ∧
      ∀ v, G'.degree v ≤ 1 := sorry

end Imo2019P3

File author(s): Kimi K3

This problem has a complete formalized solution.