Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2021P3

module

public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.RingTheory.RootsOfUnity.Complex
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 2021, Problem 3

Let n ≥ 2 be an integer. An n × n board is initially empty. Each minute, you may
perform one of three moves:

• If there is an L-shaped tromino region of three cells without stones on the
  board (see figure; rotations not allowed), you may place a stone in each of
  those cells.
• If all cells in a column have a stone, you may remove all stones from that
  column.
• If all cells in a row have a stone, you may remove all stones from that row.

For which n is it possible that, after some non-zero number of moves, the board
has no stones?
-/

namespace Usa2021P3

/- determine -/ abbrev answer : ℕ → Prop := sorry

/-- USAMO 2021 Problem 3: the board can be emptied after a non-zero number of
moves if and only if `3 ∣ n`. -/
theorem usa2021_p3 (n : ℕ) (hn : 2 ≤ n) : Solvable n ↔ answer n := sorry

end Usa2021P3

File author(s): Kimi K3

This problem has a complete formalized solution.