Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1982P1

module

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

public section


/-!
# USA Mathematical Olympiad 1982, Problem 1

A graph has 1982 points. Given any four points, there is at least one
joined to the other three. What is the smallest number of points which
are joined to 1981 points?
-/

namespace Usa1982P1

open Classical

/-- The hypothesis of the problem: among any four vertices of the graph,
some vertex is adjacent to the other three. -/
def FourPointProperty (G : SimpleGraph (Fin 1982)) : Prop :=
  ∀ s : Finset (Fin 1982), s.card = 4 → ∃ v ∈ s, ∀ w ∈ s, w ≠ v → G.Adj v w

/-- A vertex is *universal* if it is joined to all 1981 other vertices. -/
def IsUniversal (G : SimpleGraph (Fin 1982)) (v : Fin 1982) : Prop :=
  ∀ w, w ≠ v → G.Adj v w

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

theorem usa1982_p1 :
    IsLeast {n : ℕ | ∃ G : SimpleGraph (Fin 1982), FourPointProperty G ∧
      n = (Finset.univ.filter (IsUniversal G)).card} solution := sorry

end Usa1982P1

File author(s): Kimi K3

This problem has a complete formalized solution.