这篇论文证明了Vandermonde行列式偶次幂在够多变量时总缺某些单项式，用了Codex生成思路和Lean形式化，挺有意思的组合。
Monical、Tokcan和Yong的猜想被证明：对每个固定偶数幂k≥4，Vandermonde行列式的k次幂在足够多变量时是非SNP的，即牛顿多面体中存在系数为零的格点。奇数幂情况由交替性保证，二次幂情况此前已知。证明利用Dyson常项恒等式，并通过有限变量Jack内积和Macdonald特殊化公式实现。构造和证明思路来自OpenAI Codex（GPT Sol 5.6 Extra High），完整对话记录在附录。Lean形式化证明已开源在GitHub。
Powers of the Vandermonde determinant are eventually non-SNP
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.