We establish a collection of new size lower bounds against fairly strong algebraic-Boolean propositional proof systems, from depth-3 semantic polynomial calculus for CNFs, up to semantic $AC^0[2]$-Frege in the regime of deep formulas, as follows:
(1) $\Sigma\Pi\Sigma$-PC: Exponential lower bound against semantic $\Sigma\Pi\Sigma$-PC over $F_2$, namely, polynomial calculus operating with depth-3 circuits with sum top gate, for the bit pigeonhole principle. We further obtain $2^{\Omega(n)}$ lower bounds for random 3-CNFs on $n$ variables and for the bit and functional pigeonhole principles with $n+1$ pigeons and $n$ holes.
(2) $\Sigma\Pi\Sigma\Pi$-PC: Superpolynomial lower bounds for semantic $\Sigma\Pi\Sigma\Pi$-PC over $F_2$, with unrestricted bottom fan-in. The hard instances include the weak unary pigeonhole principle and lifting of random CNFs of logarithmic width. For the weak pigeonhole principle with $2n$ pigeons and $n$ holes, the lower bound is $\exp(\Omega((\log n)^2/\log\log n))$. This further settles the open problem of establishing superpolynomial lower bounds against $\mathrm{Res}(\log)$ for this principle. When the $\Sigma\Pi\Sigma\Pi$-PC bottom fan-in is logarithmic, we obtain exponential lower bounds for random CNFs of logarithmic width.
(3) Depth-$d$ $AC^0[2]$-Frege: For every fixed $d\ge 2$, we construct unsatisfiable families of formulas of depth $d$ that require superpolynomial-size semantic depth-$d$ $AC^0[2]$-Frege refutations, but have polynomial-size semantic depth-$(d+1)$ $AC^0[2]$-Frege refutations. This provides the first unconditional hard instances against arbitrary depth $AC^0[2]$-Frege.
The arguments build and expand on the recent AI-generated proof of an exponential lower bound against resolution over parities by Braun [16]. We distil Braun's implicit annihilating polynomial argument into an abstract framework based on standard pseudo-reduction operators, and augment it with new techniques. We show how rank lower bounds for these operators imply proof-size lower bounds. The polynomial approximation method of Razborov and Smolensky [60, 64] extends the framework to bounded bottom degree. Lifting and random restrictions remove the restriction on bottom fan-in. For the $AC^0[2]$-Frege result, we combine polynomial approximation with the common annihilating polynomial and a lifting construction based on constant-depth formulas for the coin problem.
