Cook and Reckhow [1] proved that NP ≠ coNP if and only if in every propositional proof system there is a tautology whose proof size has a super-polynomial lower bound (in terms of the size of the proved formula). Currently, it is not known whether even very basic proof systems, such as Frege systems, have such lower bounds.

Proof systems are also connected to circuit classes. For instance, “Frege corresponds to NC¹, and extended Frege corresponds to P/poly.” Does this correspondence between proof systems and circuit classes allow one to conclude lower bounds on a circuit class from lower bounds on the corresponding proof system? For instance, if such an implication held, a super-polynomial lower bound on Frege systems would separate NP and NC¹. However, up to now, no proof system was known whose “lower bounds imply computational complexity lower bounds of any kind.”

This paper defines a new proof system, the ideal proof system (IPS). In IPS, a certificate is a single polynomial, which certifies that a given system of polynomial equations is unsatisfiable. A proof of unsatisfiability of a given polynomial equation system is an algebraic circuit computing some unsatisfiability certificate. A key difference between IPS and other algebraic proof systems is that IPS does not require that the intermediate polynomials, computed in the process of proving, belong to the ideal generated by the original polynomials: it is enough that the final one belongs. The authors state: “This key difference allows IPS proofs to be ordinary algebraic circuits, and thus nearly all results in algebraic circuit complexity apply directly to the ideal proof system.”

A remarkable property of IPS is that its lower bounds indeed imply lower bounds in algebraic circuit complexity. Namely, any super-polynomial lower bound on a Boolean tautology in IPS implies that “the permanent does not have polynomial-size algebraic circuits” (hence, VNP ≠ VP). As a corollary, this would imply the permanent versus determinant conjecture. Also, lower bounds on bounded-depth versions of IPS would imply the corresponding algebraic circuit lower bounds. For instance, “lower bounds on the logarithmic-depth version of [IPS] imply VNP ⊈ VNC¹.” Moreover, the polynomial equivalence (that is, mutual polynomial simulation) of IPS and extended Frege has been proved, modulo some reasonable assumptions on polynomial identity testing (PIT). The authors also use PIT to understand the difficulty of proving lower bounds for AC⁰[p]-Frege, a problem that has been open for nearly 30 years.

At the end of the paper, the authors list some open problems and discuss the possibility of using techniques from algebraic circuit complexity to show proof complexity lower bounds. As mentioned in the paper, they “propose a novel route to such lower bounds.” It promises to be an intriguing journey.