The alternating sign matrix theorem

alternating_sign_matrix_count

Submitter: Kim Morrison.

Notes: The number of n×n alternating sign matrices is the Robbins product ∏_{k<n} (3k+1)!/(n+k)! (Zeilberger 1994; Kuperberg 1996). Trusted helpers (IsAlternatingSignMatrix, ASMatrix, robbinsProduct, …) are non-holes. Mathlib has no ASM enumeration. Candidate from §168 of the Knill survey.

Source: D. Zeilberger (1996); G. Kuperberg (1996). Knill, §168.

Informal solution: Unavailable.

theorem declaration uses `sorry`alternating_sign_matrix_count (n : ℕ) :
    (Nat.card (LeanEval.Combinatorics.AlternatingSignMatrix.ASMatrix n) : ℚ) = LeanEval.Combinatorics.AlternatingSignMatrix.robbinsProduct n := byn:ℕ⊢ ↑(Nat.card (ASMatrix n)) = robbinsProduct n
  sorryAll goals completed! 🐙

Solved by

Not yet solved.