Proof complexity as a computational lens lecture 19: Polynomial calculus & roots of unity encodings

Описание: Monday Jan 19, 2026
Proof complexity as a computational lens
Lecture 19: Polynomial calculus and roots of unity encodings
(Kilian Risse, Lund University)

In this lecture, we study polynomial calculus over the basis {-1, +1} (also known as polynomial calculus over the Fourier basis or, more generally, over roots of unity) and present the result by [Sokolov '20] that the pigeonhole principle (PHP) formulas are exponentially hard to refute also in this setting. The key technical notion is the concept of the diameter of a (multilinear) polynomial, which is the largest degree of any (multilinear) product of pairs of monomials in the polynomial. We show that a small polynomial calculus refutation over {-1, +1} of a PHP formula can be converted to a small-diameter refutation of a slightly smaller PHP formula, and that refutations in small diameter also have small degree. Known degree lower bounds for PHP formulas (proved in the standard basis {0, 1}) then imply that no such small refutations over {-1, +1} can exist.

This is lecture 19 on the course "Proof complexity as a computational lens" (https://jakobnordstrom.se/teaching/pr...) given during the winter of 2025/26 at the University of Copenhagen and Lund University.


For more information about MIAO seminars and/or lectures, please visit https://jakobnordstrom.se/miao-seminars/ , or go to https://jakobnordstrom.se/miao-group/ to read more about the MIAO group.

#ProofComplexity