Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi JACM 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 [FSTW21; ToC 2021]), which reduces the hardness of refuting a polynomial equation $f(\overline x) = 0$ with no Boolean solutions to the hardness of computing the function $1/f(\overline 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, hard instances different from Subset Sum variants, and hardness for stronger IPS fragments, all of which were unknown before. 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:
$\mathbf{\textbf{Nullstellensatz degree lower bounds using symmetry}}$: Extending [FSTW21] we show that every unsatisfiable symmetric polynomial with $n$ variables requires degree $>n$ refutations (over sufficiently large characteristic). Using symmetry again, by characterising the $\frac{n}{2}$-homogeneous slice appearing in refutations, we give examples of unsatisfiable invariant polynomials of degree $\frac{n}{2}$ that require degree $\ge n$ refutations.
$\mathbf{\textbf{Lifting to size lower bounds}}$: Lifting our Nullstellensatz degree bounds to IPS-size lower bounds, we obtain exponential lower bounds for any poly-logarithmic degree symmetric instance against IPS refutations written as oblivious read-once algebraic programs (roABP-IPS). For invariant polynomials, we show lower bounds against roABP-IPS and refutations written as multilinear formulas in the placeholder IPS regime (studied in [FSTW21], and Andrews-Forbes STOC 2022), where the hard instances do not necessarily have small roABPs themselves, including over positive characteristic fields. This provides the first explicit example of a hard instance against IPS fragments over finite fields.
By an adaptation of the work of Amireddy, Garg, Kayal, Saha and Thankey (ICALP 2023), we extend and strengthen the constant-depth IPS lower bounds obtained recently in Govindasamy, Hakoniemi and Tzameret (GHT22; FOCS 2022) which held only for *multilinear* proofs, to *poly$(\log \log n)$* individual degree proofs. This is a natural and stronger constant depth proof system than in [GHT22], which we show admits small refutations for standard hard instances like the pigeonhole principle and Tseitin formulas.
$\mathbf{\textbf{Barriers for Boolean instances}}$: While lower bounds against strong propositional proof systems were the original motivation for studying algebraic proof systems in the 1990s (Beame et al. 1996; Proc. London Math. Soc; Buss et al. 1996; Comput. Complex.), we show that the functional lower bound method alone cannot establish any size lower bound for *Boolean* instances for any sufficiently strong proof systems, and in particular, cannot lead to lower bounds against AC$^0[p]$-Frege and TC$^0$-Frege.
