What was already known
Monical, Tokcan and Yong proved k=1 and k=2, gave propagation lemmas and conjectured the result for every fixed power. Even powers k≥4 remained.
AI involvement
Codex found the uniform even-power exponent and cancellation strategy under Thien Le’s direction. Le and Melanie Weber checked, organized and completed the proof.
Codex supplied the retained explicit exponent and core even-power proof, while human authors posed the task, guided the exchange and checked and assembled the final argument.
Importance
The construction resolves their eventual non-SNP conjecture for all fixed powers.
Limitations
Lean checks the even-power seed, including an unconditional Ward-recurrence route. The full eventual theorem also uses earlier propagation lemmas checked in the authors’ written proof.
Technical verification
The authors report checking the full proof. The repository reports Lean verification of the even-power seed, including an assumption-free Ward proof; propagation to all sufficiently large n uses the paper's human-reviewed known lemma. The Lean scope is the seed, not every line of the full theorem.
Formal checking
Author check and organization of the resulting proof and citations
- Checker
- Thien Le and Melanie Weber
- Scope
- Full eventual non-SNP proof, including the model-origin even-power construction
- Basis
- Reported by the linked checker
Formal checking
VandermondeSNP.even_seed_statement_unconditional via Ward recurrence; separate Jack target conditional on MacdonaldJackFacts
- Checker
- Lean 4 development in steven-le-thien/vandermonde-snp
- Scope
- For m≥2 the explicit even-power seed lies in the scaled permutahedron and has vanishing Vandermonde coefficient
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The human authors explain the exact exponent, Newton-polytope membership and coefficient cancellation and supply detailed calculations.
Correction and publication history
The construction resolves their eventual non-SNP conjecture for all fixed powers.
Read this published revision