Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1985P4

module

public import Mathlib.Algebra.Order.Ring.Canonical
public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.Combinatorics.Enumerative.DoubleCounting
public import Mathlib.Combinatorics.SimpleGraph.Finite
public import Mathlib.Tactic.Choose
public import Mathlib.Tactic.GCongr
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1985, Problem 4

A graph has n > 2 points. Show that we can find two points A and B such that
at least ⌊n/2⌋ - 1 of the remaining points are joined to either both or
neither of A and B.
-/

namespace Usa1985P4

open Finset

theorem usa1985_p4 (n : ℕ) (hn : 2 < n) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    ∃ A B : Fin n, A ≠ B ∧
      n / 2 - 1 ≤ (Finset.univ.filter fun X =>
        X ≠ A ∧ X ≠ B ∧ (G.Adj X A ↔ G.Adj X B)).card := sorry

end Usa1985P4

File author(s): Kimi K3

This problem has a complete formalized solution.