Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2008P6

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Combinatorics.SimpleGraph.Finite
public import Mathlib.FieldTheory.Finiteness
public import Mathlib.RingTheory.PicardGroup

public section


/-!
# USA Mathematical Olympiad 2008, Problem 6

At a certain mathematical conference, every pair of mathematicians are
either friends or strangers. At mealtime, every participant eats in one of
two large dining rooms. Each mathematician insists upon eating in a room
which contains an even number of his or her friends. Prove that the number
of ways that the mathematicians may be split between the two rooms is a
power of two (i.e., is of the form 2^k for some positive integer k).
-/

namespace Usa2008P6

theorem usa2008_p6 (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    ∃ k : ℕ, Fintype.card {x : Fin n → ZMod 2 // ∀ v : Fin n,
      Even ((G.neighborFinset v).filter fun u => x u = x v).card} = 2 ^ k := sorry

end Usa2008P6

File author(s): Kimi K3

This problem has a complete formalized solution.