The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finite subcube of the field. This fundamental fact about multivariate polynomials has found many applications in algorithms, complexity theory, coding theory, and combinatorics. We give a new proof of the lemma that offers some advantages over the standard proof. First, the new proof is more constructive than previously known proofs. For every given side-length of the cube, the proof constructs a polynomial-time computable and polynomial-time invertible surjection onto the set of roots in the cube. The domain of the surjection is tight, thus showing that the set of roots on the cube can be compressed. Second, the new proof can be formalised in Buss' bounded arithmetic theory $\mathrm{S}^1_2$ for polynomial-time reasoning. One consequence of this is that the theory $\mathrm{S}^1_2 + \mathrm{dWPHP(PV)}$ for approximate counting can prove that the problem of verifying polynomial identities (PIT) can be solved by polynomial-size circuits. The same theory can also prove the existence of small hitting sets for any explicitly described class of polynomials of polynomial degree. To complete the picture we show that the existence of such hitting sets is \emph{equivalent} to the surjective weak pigeonhole principle $\mathrm{dWPHP(PV)}$, over the theory $\mathrm{S}^1_2$. This is a contribution to a line of research studying the reverse mathematics of computational complexity. One consequence of this is that the problem of constructing small hitting sets for such classes is complete for the class APEPP of explicit construction problems whose totality follows from the probabilistic method. This class is also known and studied as the class of Range Avoidance Problems.

翻译：Schwartz-Zippel引理指出，若系数在某个域上的低次多元多项式在该域上不恒为零，则它在域的每个有限子立方体上仅有少量根。这一关于多元多项式的基本事实在算法、复杂性理论、编码理论和组合数学中有着广泛应用。我们给出该引理的一个新证明，相较于标准证明具有若干优势。首先，新证明比以往已知的证明更具构造性。对于给定的立方体边长，该证明构造了一个从定义域到立方体内根集合的多项式时间可计算且多项式时间可逆的满射。该满射的定义域是紧致的，从而表明立方体上的根集合可以被压缩。其次，新证明可在Buss的有界算术理论$\mathrm{S}^1_2$中形式化，该理论适用于多项式时间推理。由此产生的一个推论是，用于近似计数的理论$\mathrm{S}^1_2 + \mathrm{dWPHP(PV)}$能够证明多项式恒等式验证（PIT）问题可由多项式规模电路解决。同一理论还能证明，对于任何显式描述的多项式次数多项式类，存在小的命中集。为完善理论图景，我们证明了此类命中集的存在性在理论$\mathrm{S}^1_2$上等价于满射弱鸽巢原理$\mathrm{dWPHP(PV)}$。这是对计算复杂性逆向数学研究脉络的一项贡献。由此产生的另一个推论是：为此类多项式类构造小命中集的问题，对于APEPP类（即其完全性可从概率方法导出的显式构造问题类）是完全的。该类也被称为并作为范围规避问题类被研究。