Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1989P2

module

public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.SimpleGraph.DegreeSum

public section


/-!
# USA Mathematical Olympiad 1989, Problem 2

The 20 members of a local tennis club have scheduled exactly 14 two-person
games among themselves, with each member playing in at least one game.
Prove that within this schedule can be found a set of six games with
12 distinct players.
-/

namespace Usa1989P2

open Finset

theorem usa1989_p2
    (G : SimpleGraph (Fin 20)) [DecidableRel G.Adj]
    (hcard : #G.edgeFinset = 14)
    (hdeg : ∀ v : Fin 20, 1 ≤ G.degree v) :
    ∃ s : Finset (Sym2 (Fin 20)), s ⊆ G.edgeFinset ∧ #s = 6 ∧
      #(s.biUnion Sym2.toFinset) = 12 := sorry

end Usa1989P2

File author(s): Kimi K3

This problem has a complete formalized solution.