We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas, J. ACM 2025; Forbes, CCC 2024) are hard to prove in certain proof systems. We focus on a DNF formula that expresses that such lower bounds are hard for constant-depth algebraic proofs. Using an adaptation of the diagonalization framework of Santhanam and Tzameret (SIAM J. Comput. 2025), we show unconditionally that this family of DNF formulas does not admit polynomial-size propositional AC0[p]-Frege proofs infinitely often. This rules out the possibility that the DNF family is easy, and establishes that its status is either that of a hard tautology for AC0[p]-Frege or else unprovable (not a tautology). While it remains open whether the DNFs in question are tautologies, we provide evidence in this direction. In particular, under the plausible assumption that certain weak properties of multilinear algebra, specifically those involving tensor rank, do not admit short constant-depth algebraic proofs, the DNFs are tautologies. We also observe that several weaker variants of the DNF formula are provably tautologies, and we show that the question of whether the DNFs are tautologies connects to conjectures of Razborov (ICALP 1996) and Krajicek (J. Symb. Log. 2004). Our result has two additional features. (i) Existential depth amplification: the DNF formula is parameterised by a constant depth d bounding the depth of the algebraic proofs. We show that there exists some fixed depth d such that if there are no small depth-d algebraic proofs of certain circuit lower bounds for the Permanent, then there are no such small algebraic proofs in any constant depth. (ii) Necessity: we show that our result is a necessary step towards establishing lower bounds against constant-depth algebraic proofs, and more generally against any sufficiently strong proof system.

Lower bounds against strong algebraic proof systems, and specifically fragments of the Ideal Proof System (IPS), have been obtained in an ongoing line of work. With the exception of the placeholder model, where the instance itself lacks small circuits, all existing bounds are proved only over large (or characteristic 0) fields, whereas finite fields form the more natural setting for propositional proof complexity. This work establishes lower bounds against fragments of IPS over constant-sized finite fields, resolving an open problem left by a series of prior works beginning with Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.’21), persisting with Behera, Limaye, Ramanathan, and Srinivasan (ICALP’25), and most recently posed by Forbes (CCC’24). We further highlight the importance of the constant-sized finite field regime in IPS by showing that any hard instance in this regime for a sufficiently strong proof system translates into a hard instance against AC0[p]-Frege, whose lower bounds remain a longstanding open problem.

Given two symbolic matrices X and Y of dimensions m × n and n × m, respectively, the rank principle states that when m = n+1 and A is a scalar matrix of rank n+1, the equation XY = A is unsatisfiable. When m is arbitrarily larger than n and A has rank exceeding n, we obtain the weak rank principle. We study this principle as an algebraic generalisation of the weak pigeonhole principle (WPHP), asserting that m pigeons cannot be injected into n holes, extending its counting argument to an algebraic setting. As a strengthening of WPHP, it admits proof complexity lower bounds in settings where none are known for WPHP, yet we show that these still yield applications analogous to those of WPHP. In particular, using new generalised types of random restrictions, which may be interesting by themselves, this allows us to resolve a number of open problems in proof complexity, including the construction of proof complexity generators for Polynomial Calculus Resolution over the two-element field (PCRF2), new generators for Sherali–Adams (SA), and hardness results for circuit lower bound statements against PCRF2, as detailed below.

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 S21 for polynomial-time reasoning. One consequence of this is that the theory S21 + 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 equivalent to the surjective weak pigeonhole principle dWPHP(PV), over the theory S21. 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.

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

We develop the theory of cryptographic nondeterministic-secure pseudorandomness beyond the point reached by Rudich’s original work [S. Rudich, 1997], and apply it to draw new consequences in average-case complexity and proof complexity. Specifically, we show the following: Demi-bit stretch: Super-bits and demi-bits are variants of cryptographic pseudorandom generators which are secure against nondeterministic statistical tests [S. Rudich, 1997]. They were introduced to rule out certain approaches to proving strong complexity lower bounds beyond the limitations set out by the Natural Proofs barrier of Razborov and Rudich [A. A. Razborov and S. Rudich, 1997]. Whether demi-bits are stretchable at all had been an open problem since their introduction. We answer this question affirmatively by showing that: every demi-bit b:{0,1}ⁿ → {0,1}^{n+1} can be stretched into sublinear many demi-bits b':{0,1}ⁿ → {0,1}^{n+n^{c}}, for every constant 0 < c < 1. Average-case hardness: Using work by Santhanam [Rahul Santhanam, 2020], we apply our results to obtain new average-case Kolmogorov complexity results: we show that K^{poly}[n-O(1)] is zero-error average-case hard against NP/poly machines iff K^{poly}[n-o(n)] is, where for a function s(n):ℕ → ℕ, K^{poly}[s(n)] denotes the languages of all strings x ∈ {0,1}ⁿ for which there are (fixed) polytime Turing machines of description-length at most s(n) that output x. Characterising super-bits by nondeterministic unpredictability: In the deterministic setting, Yao [Yao, 1982] proved that super-polynomial hardness of pseudorandom generators is equivalent to ("next-bit") unpredictability. Unpredictability roughly means that given any strict prefix of a random string, it is infeasible to predict the next bit. We initiate the study of unpredictability beyond the deterministic setting (in the cryptographic regime), and characterise the nondeterministic hardness of generators from an unpredictability perspective. Specifically, we propose four stronger notions of unpredictability: NP/poly-unpredictability, coNP/poly-unpredictability, ∩-unpredictability and ∪-unpredictability, and show that super-polynomial nondeterministic hardness of generators lies between ∩-unpredictability and ∪-unpredictability. Characterising super-bits by nondeterministic hard-core predicates: We introduce a nondeterministic variant of hard-core predicates, called super-core predicates. We show that the existence of a super-bit is equivalent to the existence of a super-core of some non-shrinking function. This serves as an analogue of the equivalence between the existence of a strong pseudorandom generator and the existence of a hard-core of some one-way function [Goldreich and Levin, 1989; Håstad et al., 1999], and provides a first alternative characterisation of super-bits. We also prove that a certain class of functions, which may have hard-cores, cannot possess any super-core.

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 2018]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson ‍[Theory ‍Comput., 17: 1-88, 2021]), which reduces the hardness of refuting a polynomial equation f(x)=0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method. This includes hardness over finite fields and hard instances different from Subset Sum variants both of which were unknown before, and stronger constant-depth lower bounds. Conversely, we expose the limitation of this method by showing it cannot lead to proof complexity lower bounds for any hard Boolean instance (e.g., CNFs) for any sufficiently strong proof systems. Specifically, we show the following:

Abstract. We introduce the binary value principle, which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi [ J. ACM, 65 (2018), 37]. Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semialgebraic proof systems. Our results extend to unrestricted IPS the paradigm introduced by Forbes, Shpilka, Tzameret, and Wigderson [ Theory Comput., 17 (2021), pp. 1–88], whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semialgebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following. (1) Conditional IPS lower bounds: The Shub–Smale hypothesis [ Duke Math. J., 81 (1995), pp. 47–54] implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation [Formula: see text] for Boolean [Formula: see text]’s. Further, the related and more widely known [Formula: see text]-conjecture [ Duke Math. J., 81 (1995), pp. 47–54] implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or apparently weaker propositional proof systems such as Frege systems (though our lower bounds do not translate to Frege lower bounds since the hard instances are not Boolean formulas). (2) Algebraic versus semialgebraic proofs: Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semialgebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semialgebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semialgebraic analogue of the IPS: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sum-of-squares proofs (and extensions) as algebraic circuits. We prove that IPS polynomially simulates CPS iff IPS admits polynomial-size refutations of the binary value principle (for the language of systems of equations that have no 0/1-solutions), over both [Formula: see text] and [Formula: see text].

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\displaystyle \sum_{i,j,k,\ell\in[n]}Z_{i_{J}^{\prime}k}\ell x_{i}x_{j}x_{k}x_{\ell}-\beta=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews and Forbes (STOC’22) established recently a constant-depth IPS lower bound, but their hard instance does not have itself small constant-depth circuits, while our instance is computable already with small depth-2 circuits. Our argument relies on extending the recent breakthrough lower bounds against constant-depth algebraic circuits by Limaye, Srinivasan and Tavenas (FOCS’21) to the functional lower bound framework of Forbes, Shpilka, Tzameret and Wigderson (ToC’21), and may be of independent interest. Specifically, we construct a polynomial f computable with small-size constant-depth circuits, such that the multilinear polynomial computing $1/f$ over Boolean values and its appropriate set-multilinear projection are hard for constant-depth circuits.

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms [3]: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems (cf. [4]). Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds.This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones.We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz’s [7] dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted $${\rm Res}({\rm lin}_R)$$ , this refutation system operates with disjunctions of linear equations with Boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of Raz & Tzameret (2008), through the work of Itsykson & Sokolov (2020) which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. Garlik & Kołodziejczyk 2018; Itsykson & Sokolov 2020; Krajícek 2017; Krajícek & Oliveira 2018) made it evident that establishing lower bounds against general $${\rm Res}({\rm lin}_R)$$ refutations is a challenging and interesting task since the system captures a ``minimal'' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds against general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular, we prove that the subset-sum principle $$1+\sum\nolimits_{i=1}^{n}2^i x_i = 0$$ requires refutations of exponential size over $$\mathbb{Q}$$ . We use a novel lower bound technique: We show that under certain conditions every refutation of a subset-sum instance $$f=0$$ must pass through a fat clause consisting of the equation $$f=\alpha$$ for every $$\alpha$$ in the image of f under Boolean assignments, or can be efficiently reduced to a proof containing such a clause. We then modify this approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. We then turn to the finite fields regime, showing that the work of Itsykson & Sokolov (2020), where tree-like lower bounds over $$\mathbb{F}_2$$ were obtained, can be carried over and extended to every finite field. We establish new lower bounds and separations as follows: (i) For every pair of distinct primes $$p,q$$ , there exist CNF formulas with short tree-like refutations in $${\rm Res}({\rm lin}{\mathbb{F}_p})$$ that require exponential-size tree-like $${\rm Res}({\rm lin}{\mathbb{F}_q})$$ refutations; (ii) random k-CNF formulas require exponential-size tree-like $${\rm Res}({\rm lin}{\mathbb{F}_p})$$ refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like $${\rm Res}({\rm lin}{\mathbb{F}})$$ refutations of the pigeonhole principle, for every field $$\mathbb{F}$$ .

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF (2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC 2 ; the latter is a first-order theory corresponding to the complexity class NC 2 consisting of problems solvable by uniform families of polynomial-size circuits and O (log 2 n )-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC 2 -circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field).

This talk explores the question of what does logic and specifically proof theory can tell us about the fundamental hardness questions in computational complexity. We start with a brief description of the main concepts behind bounded arithmetic which is a family of weak formal theories of arithmetic that mirror in a precise manner the world of propositional proofs: if a statement of a given form is provable in a given bounded arithmetic theory then the same statement is suitably translated to a family of propositional formulas with short (polynomial-size) proofs in a corresponding propositional proof system. We will proceed to describe the motivations behind the study of bounded arithmetic theories, their corresponding propositional proof systems, and how they relate to the fundamental complexity class separations and circuit lower bounds questions in computational complexity. We provide a collage of results and recent developments showing how bounded arithmetic and propositional proof complexity form a cohesive framework in which both concrete combinatorial questions about complexity as well as meta-mathematical questions about provability of statements of complexity theory itself, are studied. Specific topics we shall mention are: (i) The bounded reverse mathematics program [Stephen Cook and Phuong Nguyen, 2010]: studying the weakest possible axiomatic assumptions that can prove important results in mathematics and computing (cf. [Iddo Tzameret and Stephen A. Cook, 2017; Pavel Hrubeš and Iddo Tzameret, 2015]), and the correspondence between circuit classes and theories. (ii) The meta-mathematics of computational complexity: what kind of reasoning power do we need in order to prove major results in complexity theory itself, and applications to complexity lower bounds (cf. [Razborov, 1995; Rahul Santhanam and Jan Pich, 2019]). (iii) Proof complexity: the systematic treatment of propositional proofs as combinatorial and algebraic objects and their algorithmic applications (cf. [Samuel Buss, 2012; Tonnian Pitassi and Iddo Tzameret, 2016; Noah Fleming et al., 2019]).

We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following:

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any superpolynomial-size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity and among a handful of fundamental hardness questions in complexity theory. Noncommutative algebraic formulas, on the other hand, constitute a quite weak computational model, for which exponential-size lower bounds were shown back in 1991 by Nisan [ Proceedings of STOC, 1991, pp. 410--418], using a particularly transparent argument. In this work we show that Frege lower bounds in fact follow from size lower bounds on noncommutative formulas computing certain families of polynomials (and that such lower bounds on noncommutative formulas must exist, unless ( NP=coNP). More precisely, we demonstrate a natural association between tautologies $T$ to families of noncommutative polynomials $P$ such that if $T$ has a polynomial-size Frege proof, then some noncommutative polynomial in $P$ can be computed by a polynomial-size noncommutative algebraic formula, and conversely, when $T$ is a formula in disjunctive normal form, if some polynomial in $P$ has a polynomial-size noncommutative algebraic formula over $GF(2)$, then $T$ has a Frege proof of quasi-polynomial size. The argument is a characterization of Frege proofs as noncommutative formulas: we show that the Frege system is (quasi-) polynomially equivalent to a noncommutative ideal proof system(IPS), following the recent work of Grochow and Pitassi [ Proceedings of FOCS, 2014, pp. 110--119] that introduced a propositional proof system in which proofs are algebraic circuits and the work in [I. Tzameret, Inform. Comput., 209 (2011), pp. 1269--1292] that considered adding the commutator as an axiom in algebraic propositional proof systems. This also gives a characterization of propositional Frege proofs in terms of (noncommutative) algebraic formulas that is tighter than (the formula version of IPS) in Grochow and Pitassi [ Proceedings of FOCS, 2014, pp. 110--119].

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs, where proof-lines are circuits from restricted boolean circuit classes. Except one, all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). We give two general methods of converting certain algebraic lower bounds into proof complexity ones. Our methods require stronger notions of lower bounds, which lower bound a polynomial as well as an entire family of polynomials it defines. Our techniques are reminiscent of existing methods for converting boolean circuit lower bounds into related proof complexity results, such as feasible interpolation. We obtain the relevant types of lower bounds for a variety of classes (sparse polynomials, depth-3 powering formulas, read-once oblivious algebraic branching programs, and multilinear formulas), and infer the relevant proof complexity results. We complement our lower bounds by giving short refutations of the previously-studied subset-sum axiom using IPS subsystems, allowing us to conclude strict separations between some of these subsystems.

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e. Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. Non-commutative arithmetic formulas, on the other hand, constitute a quite weak computational model, for which exponential-size lower bounds were shown already back in 1991 by Nisan [STOC 1991], using a particularly transparent argument. In this work we show that Frege lower bounds in fact follow from corresponding size lower bounds on non-commutative formulas computing certain polynomials (and that such lower bounds on non-commutative formulas must exist, unless NP=coNP). More precisely, we demonstrate a natural association between tautologies T to non-commutative polynomials p, such that: (*) if T has a polynomial-size Frege proof then p has a polynomial-size non-commutative arithmetic formula; and conversely, when T is a DNF, if p has a polynomial-size non-commutative arithmetic formula over GF(2) then T has a Frege proof of quasi-polynomial size. The argument is a characterization of Frege proofs as non-commutative formulas: we show that the Frege system is (quasi-)polynomially equivalent to a non-commutative Ideal Proof System (IPS), following the recent work of Grochow and Pitassi [FOCS 2014] that introduced a propositional proof system in which proofs are arithmetic circuits, and the work in [Tzameret 2011] that considered adding the commutator as an axiom in algebraic propositional proof systems. This gives a characterization of propositional Frege proofs in terms of (non-commutative) arithmetic formulas that is tighter than (the formula version of IPS) in Grochow and Pitassi [FOCS 2014], in the following sense: (i) The non-commutative IPS is polynomial-time checkable - whereas the original IPS was checkable in probabilistic polynomial-time; and (ii) Frege proofs unconditionally quasi-polynomially simulate the non-commutative IPS - whereas Frege was shown to efficiently simulate IPS only assuming that the decidability of PIT for (commutative) arithmetic formulas by polynomial-size circuits is efficiently provable in Frege.

We study arithmetic proof systems ${\mathbb P}_c({\mathbb F})$ and $ {\mathbb P}_f({\mathbb F})$ operating with arithmetic circuits and arithmetic formulas, respectively, and that prove polynomial identities over a field ${\mathbb F}$. We establish a series of structural theorems about these proof systems, the main one stating that ${\mathbb P}_c({\mathbb F})$ proofs can be balanced: if a polynomial identity of syntactic degree $ d $ and depth $k$ has a ${\mathbb P}_c({\mathbb F})$ proof of size $s$, then it also has a ${\mathbb P}_c({\mathbb F})$ proof of size $ {\rm poly}(s,d) $ in which every circuit has depth $ O(k+\log^2 d + \log d\cdot \log s) $. As a corollary, we obtain a quasi-polynomial simulation of ${\mathbb P}_c({\mathbb F})$ by ${\mathbb P}_f({\mathbb F})$. Using these results we obtain the following: consider the identities $\det(XY) = \det(X)\cdot\det(Y) \mbox{ and } \det(Z)= z_{11}\cdots z_{nn},$ where $X,Y$, and $ Z$ are $n\times n$ square matrices and $Z$ is a triangular matrix with $z_{11},\dots, z_{nn}$ on the diagonal (and $ \det $ is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit $\det$ such that the above identities have ${\mathbb P}_c({\mathbb F})$ proofs of polynomial size using circuits of $ O(\log^2 n)$ depth. Moreover, there exists an arithmetic formula $ \det $ of size $n^{O(\log n)}$ such that the above identities have ${\mathbb P}_f({\mathbb F})$ proofs of size $n^{O(\log n)}$. This yields a solution to a basic open problem in propositional proof complexity, namely, whether there are polynomial-size $\mathbf{NC}^2$-Frege proofs for the determinant identities and the hard matrix identities, as considered, e.g., in Soltys and Cook [Ann. Pure Appl. Logic, 130 (2004), pp. 277--323] (cf. Beame and Pitassi [Bull. Eur. Assoc. Theor. Comput. Sci. EATCS, 65 (1998), pp. 66--89]). We show that matrix identities like $ AB=I \rightarrow BA=I $ (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size $\mathbf{NC}^2$-Frege proofs and quasi-polynomial-size Frege proofs.

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Ω(n1.5-ε) clauses (Chvatal and Szemeredi [13], Ben-Sasson and Wigderson [9]). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Ω(n2/ log n) clauses, shown by Beame et al. [5]. In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomialsize propositional refutations whose lines are TC0formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and Ω(n1.4) clauses. The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek [19]. Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic and use a general translation scheme to propositional proofs.

We study arithmetic proof systems Pc(F) and Pf(F) operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field F. We establish a series of structural theorems about these proof systems, the main one stating that Pc(F) proofs can be balanced: if a polynomial identity of syntactic degree d and depth k has a Pc(F) proof of size s, then it also has a Pc(F) proof of size poly(s,d) and depth O(k+log2 d + log d• log s). As a corollary, we obtain a quasipolynomial simulation of Pc(F) by Pf(F), for identities of a polynomial syntactic degree. Using these results we obtain the following: consider the identities: det(XY) = det(X)•det(Y) and det(Z)= z11 ••• znn, where X,Y and Z are n x n square matrices and Z is a triangular matrix with z11,..., znn on the diagonal (and det is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit det such that the above identities have Pc(F) proofs of polynomial-size and O(log2n) depth. Moreover, there exists an arithmetic formula det of size nO(log n) such that the above identities have Pf(F) proofs of size nO(log n).

We study—within the framework of propositional proof complexity—the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where many stands for an explicitly specified function Λ in the number of variables n . To this end, we develop propositional proof systems under different measures of promises (i.e., different Λ) as extensions of resolution. This is done by augmenting resolution with axioms that, roughly, can eliminate sets of truth assignments defined by Boolean circuits. We then investigate the complexity of such systems, obtaining an exponential separation in the average case between resolution under different size promises: (1) Resolution has polynomial-size refutations for all unsatisfiable 3CNF formulas when the promise is ϵ…2 n , for any constant 0<ϵ<1. (2) There are no subexponential size resolution refutations for random 3CNF formulas, when the promise is 2 Δ n , for any constant 0<δ<1 (and the number of clauses is O ( n 3/2-ϵ ), for 0<ϵ<1/2). “ Goods Satisfactory or Money Refunded ” —The Eaton Promise

Devising an efficient deterministic - or even a non-deterministic sub-exponential time - algorithm for testing polynomial identities is a fundamental problem in algebraic complexity and complexity at large. Motivated by this problem, as well as by results from proof complexity, we investigate the complexity of proving polynomial identities. To this end, we study a class of equational proof systems, of varying strength, operating with polynomial identities written as arithmetic formulas over a given ring. A proof in these systems establishes that two arithmetic formulas compute the same polynomial, and consists of a sequence of equations between polynomials, written as arithmetic formulas, where each equation in the sequence is derived from previous equations by means of the polynomial-ring axioms. We establish the first non-trivial upper and lower bounds on the size of equational proofs of polynomial identities, as follows: 1. Polynomial-size upper bounds on equational proofs of identities involving symmetric polynomials and interpolation-based identities. In particular, we show that basic properties of the elementary symmetric polynomials are efficiently provable already in equational proofs operating with depth-4 formulas, over infinite fields. This also yields polynomial-size depth-4 proofs of the Newton identities, providing a positive answer to a question posed by Grigoriev and Hirsch. 2. Exponential-size lower bounds on (full, unrestricted) equational proofs of identities over certain specific rings. 3. Exponential-size lower bounds on analytic proofs operating with depth-3 formulas, under a certain regularity condition. The "analytic" requirement is, roughly, a condition that forbids introducing arbitrary formulas in a proof and the regularity condition is an additional structural restriction. 4. Exponential-size lower bounds on one-way proofs (of unrestricted depth) over infinite fields. Here, one-way proofs are analytic proofs, in which one is also not allowed to introduce arbitrary constants. Furthermore, we determine basic structural characterizations of equational proofs, and consider relations with polynomial identity testing procedures. Specifically, we show that equational proofs efficiently simulate the polynomial identity testing algorithm provided by Dvir and Shpilka.