The Colomo-Pronko conjecture for frozen-corner alternating sign matrices
Yinjie Li
math.CO
Sep 13, 2026 · v1
math.PR
TL;DR
The finite-dimensional algebraic core of the proof, including the inverse commutator identity, was formalized in Lean 4.
Abstract
We prove the Colomo-Pronko conjecture for alternating sign matrices with a prescribed square of zeros at a corner, for all matrix sizes and freezing parameters. A known multiple-integral formula for the frozen-corner count yields determinant representations built from fixed polynomial kernels. We relate these kernels to the conjectured determinant through an inverse identity for the commutator of a signed Pascal matrix with reversal. In odd dimension, the comparison uses the one-dimensional nullspace and projection along it to eliminate the central coordinate. Combined with the asymptotic analysis of Colomo and Pronko, our result removes the conjectural assumption from their GUE Tracy-Widom fluctuation theorem for the intersection of the frozen boundary with the main diagonal in uniformly random alternating sign matrices. The finite-dimensional algebraic core of the proof has been formalized in Lean 4.
Problem
The Colomo-Pronko conjecture proposes a determinant formula counting n×n alternating sign matrices with a prescribed s×s square of zeros at a corner. Proving it would remove a conjectural assumption from the GUE Tracy-Widom fluctuation theorem for the frozen boundary's intersection with the main diagonal.
Approach
A known multiple-integral formula for the frozen-corner count yields determinant representations built from fixed polynomial kernels. These kernels are related to the conjectured determinant via an inverse identity for the commutator of a signed Pascal matrix with reversal. In odd dimension, the comparison uses the one-dimensional nullspace and projection along it to eliminate the central coordinate. The finite-dimensional algebraic core was formalized in Lean 4.
Results
The conjecture is proven for all matrix sizes n and freezing parameters s. Combined with Colomo-Pronko's asymptotic analysis, this establishes the GUE Tracy-Widom fluctuation theorem unconditionally.
