alternating_sign_matrix_count.toml

id = "alternating_sign_matrix_count"
title = "The alternating sign matrix theorem"
test = false
module = "LeanEval.Combinatorics.AlternatingSignMatrix"
holes = ["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."