Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2014P4

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2014, Problem 4

Let k be a positive integer. Two players A and B play a game on an infinite
grid of regular hexagons. Initially all the grid cells are empty. Then the
players alternately take turns with A moving first. In her move, A may choose
two adjacent hexagons in the grid which are empty and place a counter in both
of them. In his move, B may choose any counter on the board and remove it.
If at any time there are k consecutive grid cells in a line all of which
contain a counter, A wins. Find the minimum value of k for which A cannot
win in a finite number of moves, or prove that no such minimum value exists.

The answer is `k = 6`.
-/

namespace Usa2014P4

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

theorem usa2014_p4 : IsLeast {k : ℕ | 0 < k ∧ ¬ ACanWin k} solution := sorry

end Usa2014P4

File author(s): Kimi K3

This problem has a complete formalized solution.