Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1999P5

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Algebra.Group.Action.Defs
public import Mathlib.Algebra.Ring.Parity
public import Mathlib.Tactic.DeriveFintype

public section


/-!
# USA Mathematical Olympiad 1999, Problem 5

The Y2K Game is played on a 1 × 2000 grid as follows. Two players in turn write either
an S or an O in an empty square. The first player who produces three consecutive boxes
that spell SOS wins. If all boxes are filled without producing SOS then the game is a draw.
Show that the second player has a winning strategy.
-/

namespace Usa1999P5

theorem usa1999_p5 :
    ∃ σ : Strategy, ∀ τ : Strategy, play 2001 τ σ (fun _ => none) true = Outcome.p2 := sorry

end Usa1999P5

File author(s): Kimi K3

This problem has a complete formalized solution.