Alon’s Combinatorial Nullstellensatz

Arthur Freitas Ramos 📧, Ruy Jose Guerra Barretto de Queiroz and David Barros Hulak

May 10, 2026

Abstract

This entry formalizes Alon’s Combinatorial Nullstellensatz for sparse multivariate polynomials over fields. The proof derives the coefficient formula from univariate Lagrange interpolation and uses it to obtain the standard nonvanishing conclusion over finite grids. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.

License

BSD License

Note

codex with gpt 5.5 on xhigh reasoning was used to help with proof engineering

Topics

Session Combinatorial_Nullstellensatz

Cite

× 
@article{Combinatorial_Nullstellensatz-AFP,
  author  = {Arthur Freitas Ramos and Ruy Jose Guerra Barretto de Queiroz and David Barros Hulak},
  title   = {Alon’s Combinatorial Nullstellensatz},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Combinatorial_Nullstellensatz.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download