Powers of the Vandermonde determinant are eventually non-SNP
Thien Le, Melanie Weber
math.CO
Jul 26, 2026 · v1
TL;DR
An accompanying Lean formalization verifies the combinatorial proof that fixed powers of the Vandermonde determinant are eventually non-SNP.
Abstract
We prove a conjecture of Monical, Tokcan, and Yong that every fixed positive power of the Vandermonde determinant is non-SNP in all sufficiently many variables, where a polynomial is non-SNP if there is a lattice point in its Newton polytope that does not appear with nonzero coefficient. This means our result proves that for every even power $k\geq4$, there is always such a missing lattice monomial in large enough dimensions. The odd case follows from alternation, and the quadratic case was previously known. For every even power $k\geq4$, we exhibit an explicit lattice point in the Newton polytope of $a_{δ_k}^k$ whose coefficient vanishes. The vanishing is obtained from a Dyson constant-term identity, proved using the finite-variable Jack scalar product and Macdonald's specialization formula. The key even-power construction and proof strategy arose from prompting with OpenAI Codex (GPT Sol 5.6 Extra High), a large language model; the complete transcript appears in the appendix. The authors subsequently checked and organized the argument. The accompanying Lean formalization is available at
https://github.com/steven-le-thien/vandermonde-snp.
Problem
Monical, Tokcan, and Yong conjectured that every fixed positive power of the Vandermonde determinant is non-SNP in sufficiently many variables, meaning its Newton polytope contains a lattice point with vanishing coefficient.
Approach
For each even power k >= 4, an explicit lattice point in the Newton polytope of a_{delta_k}^k is exhibited whose coefficient vanishes. The vanishing follows from a Dyson constant-term identity established via the finite-variable Jack scalar product and Macdonald's specialization formula. The odd case follows from skew-symmetry and the quadratic case was known. A Lean formalization accompanies the proof.
Results
The conjecture is proven: every fixed positive power of the Vandermonde determinant is eventually non-SNP, with explicit missing lattice monomials given for even powers k >= 4.