Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2015P4

module

public import Mathlib.Data.Multiset.Sort
public import Mathlib.Data.Sym.Card
public import Mathlib.SetTheory.Cardinal.Finite

public section


/-!
# USA Mathematical Olympiad 2015, Problem 4

Steve is piling m ≥ 1 indistinguishable stones on the squares of an n × n grid.
Each square can have an arbitrarily high pile of stones. After he finished piling
his stones in some manner, he can then perform stone moves, defined as follows.
Consider any four grid squares, which are corners of a rectangle, i.e. in positions
(i, k), (i, l), (j, k), (j, l) for some 1 ≤ i, j, k, l ≤ n, such that i < j and
k < l. A stone move consists of either removing one stone from each of (i, k) and
(j, l) and moving them to (i, l) and (j, k) respectively, or removing one stone
from each of (i, l) and (j, k) and moving them to (i, k) and (j, l) respectively.

Two ways of piling the stones are equivalent if they can be obtained from one
another by a sequence of stone moves. How many different non-equivalent ways can
Steve pile the stones on the grid?
-/

namespace Usa2015P4

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

theorem usa2015_p4 (m n : ℕ) (hm : 1 ≤ m) (hn : 1 ≤ n) :
    Nat.card (Quotient (pilingSetoid m n)) = solution m n := sorry

end Usa2015P4

File author(s): Kimi K3

This problem has a complete formalized solution.