Email Gateway (May 10 2026 at 14:49): Email Gateway (May 10 2026 at 14:49):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce another contribution by Arthur Freitas Ramos, Ruy Jose Guerra Barretto de Queiroz and David Barros Hulak: Alon’s Combinatorial Nullstellensatz
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.
https://isa-afp.org/entries/Combinatorial_Nullstellensatz.html
Last updated: May 23 2026 at 03:31 UTC