{"id":"3f87df71-cd21-46a6-ac0b-3298275d07b6","arxiv_id":"2412.20114","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"New IPS lower bounds via symmetry and lifting, including finite-field instances, plus a barrier theorem ruling out functional lower bounds for Boolean instances against strong proof systems.","lead":"This paper proves new lower bounds for algebraic proof systems using symmetry and lifting, including the first such lower bounds over finite fields. It also shows that the functional lower bound method cannot prove lower bounds for Boolean formulas like CNFs against strong proof systems.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 48 in §6.1.1 is false as stated: a simple counterexample invalidates the proof of Theorem 44's constant-depth lower bounds for individual degree >1.","rationale":"The reader accepted the paper, flagging as weakest the AND-introduction assumption behind the barrier theorem. My stress-test found a more acute problem in the positive constant-depth section. The central barrier argument in Section 7 is careful and appears sound; the finite-field roABP/multilinear results (Thm 41) also appear broadly correct, though the multilinear-formula portion uses only a 2^n coefficient-dimension lower bound where full 2^{2n} seems needed—this separate gap should also be checked. The decisive issue is Lemma 48. A false lemma in the proof chain of Theorem 44 is not a matter of exposition: it breaks the claimed strengthening to O(log log n) individual degree. The concrete counterexample is simple enough to verify by hand, so the concern is not speculative. If the lemma is repaired, the paper may need only a revised proof; if not, the constant-depth claims must be weakened or removed. Given the substantial correct contributions, I recommend CONDITIONAL rather than REJECT.","tokens_in":59241,"tokens_out":40049,"duration_ms":396782,"concrete_test":"Verify Lemma 48 with t=2, Q_1=x_1^2, Q_2=x_2^2, d=2, δ=2, k=1: check whether 2x_1x_2^2 lies in the RHS span. It does not, so Lemma 48 is false. Then test the natural repair: replace the condition by k0+(k/(d'−k))ℓ0≤k−residue_k(d'_i)/δ on the same example; if the inclusion holds, re-derive Corollary 49 and Theorem 44 with this corrected parameter, and check whether the δ^2 term in the final bound remains valid.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Lemma 48 claims that for homogeneous Q_i of degrees d'_i with d' in [d, δd] and k < d, ⟨∂^k(Q_1···Q_t)⟩ is contained in Σ_{S,k0,ℓ0: k0+(k/(d−k))ℓ0 ≤ k−residue_k(d'_i)/δ} ⟨x^{ℓ0}∂^{k0}(∏_{i∈S}Q_i)⟩. This is false. Take t=2, Q_1=x_1^2, Q_2=x_2^2, so d'=4; let d=2, δ=2, k=1. Then residue_k(2,2)=1/2, so the allowed pairs are k0+ℓ0≤3/4, hence only k0=ℓ0=0. The RHS is span{1,Q_1,Q_2,Q_1Q_2}, which does not contain ∂_{x_1}(Q_1Q_2)=2x_1x_2^2. The proof sketch contains an incorrect algebraic identity: |κ_i|−(k/(d−k))(d'_i−|κ_i|) is not equal to (δd/(d−k))(|κ_i|−(k/(δd))d'_i) unless δ=1. Since Corollary 49, Lemma 53, Lemma 59, and Theorem 44 all rely on Lemma 48, the claimed constant-depth IPS lower bounds for O(log log n) individual degree are unproven as written. A corrected version might use d' in the denominator (k/(d'−k)) and rework the δ-dependence, but that is not what the paper states.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops lower bounds for fragments of the Ideal Proof System (IPS) via the functional lower bound method. It claims Nullstellensatz degree lower bounds for symmetric and vector-invariant polynomial instances, lifts these to size lower bounds against roABP-IPSLIN' and multilinear-formula-IPS refutations (including the first IPS-fragment lower bounds over finite fields), proves constant-depth IPS lower bounds for refutations of bounded individual degree, and establishes a barrier theorem showing that the functional lower bound method cannot yield lower bounds for Boolean instances against sufficiently strong proof systems such as AC0[p]-Frege and TC0-Frege. The paper positions these results as extending FSTW21 and GHT22 and as resolving a question from AGK+23.","tokens_in":59585,"tokens_out":11974,"duration_ms":119067,"significance":"If correct, the results are significant: they give new hard instances beyond subset-sum variants, the first IPS fragment lower bounds over finite fields, a strengthened constant-depth lower bound, and a clean limitation result for the functional method. The vector-invariant results in Sections 3.2 and 5 and the barrier argument in Section 7 are largely self-contained and the barrier theorem is elegant. However, two load-bearing technical statements are false as written: Claim 26 in Section 3.1 and Lemma 48 in Section 6.1.1. The latter in particular invalidates the claimed constant-depth lower bounds of Theorem 44. The results are likely repairable, but the manuscript requires substantial revision before the advertised theorems can be accepted.","major_comments":[{"comment":"Claim 26 is false as stated. For example, with n=3, d=1, k=1, we have e1,3(x)·e1,3(x) = e1,3(x) + 2e2,3(x) modulo x^2−x, whereas the claim asserts 4e2,3(x) plus lower-degree terms. The error is in Eq. (26.1): for a fixed (d+k)-subset c, the number of ordered disjoint pairs (a,b) with a∪b=c and |a|=d, |b|=k is the binomial coefficient C(d+k,d), not 2^{d+k}. Because Lemma 25 and Corollary 27 identify the leading elementary-symmetric term using this coefficient, the proof of the symmetric Nullstellensatz degree lower bound is invalid as written. Replacing 2^{d+k} by C(d+k,d) appears to preserve the intended conclusion (the coefficient is nonzero when the characteristic exceeds d+k), but the argument must be explicitly corrected.","section":"§3.1, Claim 26 and Eq. (26.1)"},{"comment":"Lemma 48 is false as stated, and the constant-depth bounded-individual-degree lower bounds built on it are therefore unproven. Counterexample: let t=2, Q1=x1^2, Q2=x2^2, d=2, δ=2, and k=1. Then d'=4 and residue_1(2,2)=1/2, so the condition in the RHS is k0 + (k/(d−k))ℓ0 = k0+ℓ0 ≤ 3/4. The only nonnegative integer pair is k0=ℓ0=0, so the RHS is span{1, x1^2, x2^2, x1^2x2^2}, which does not contain ∂_{x1}(Q1Q2)=2x1x2^2. The proof sketch also contains an incorrect algebraic identity: |κ_i| − (k/(d−k))(d'_i−|κ_i|) equals (d/(d−k))|κ_i| − kd'_i/(d−k), not (δd/(d−k))(|κ_i| − (k/(δd))d'_i) unless δ=1. Since Corollary 49, Lemma 53, Lemma 59, and Theorem 44 all rely on Lemma 48, Theorem 44 and the claimed strengthening of GHT22 are not established by the present manuscript.","section":"§6.1.1, Lemma 48"}],"minor_comments":[{"comment":"The maximization condition in Corollary 49 writes residue_k(d1,...,dt)/δ, but the lemma concerns degrees d'_1,...,d'_t; it should read residue_k(d'_1,...,d'_t)/δ for consistency with Lemma 48.","section":"§6.1.1, Corollary 49"},{"comment":"The displayed formula for α contains a typo: '∑_{ν=0}^{Δ−1} (−1)^nu τ^{2ν−1}' should presumably be '∑_{ν=0}^{Δ−1} (−1)^ν τ^{2^ν−1}'.","section":"§6.1.2, Lemma 51 proof sketch"},{"comment":"The statements say m=(n choose 2), but the lift in Eq. (35.3) is defined with m=(2n choose 2) and w={w_{i,j}}_{i<j∈[2n]}. The bound char(F) > max(24n+2m, nd) and the number of z-variables should be checked against the correct value of m.","section":"§4.1.2, Proposition 37 and Corollary 38"}],"recommendation":"major_revision","confidential_remarks":"The reader's report recommends acceptance, but it appears to overlook two concrete technical falsehoods: Claim 26's coefficient 2^{d+k} is not the number of disjoint unions, and Lemma 48 has the counterexample described above. Both are load-bearing, and the constant-depth result (Theorem 44) is not proven as written. The vector-invariant and barrier portions may well survive, and the errors look repairable, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is a substantial paper, but don't trust Section 6 as it stands. The claimed constant-depth IPS lower bounds for individual degree >1 rest on Lemma 48, and Lemma 48 is false as stated. The stress-test counterexample is correct: take Q1=x1^2, Q2=x2^2, d=2, δ=2, k=1. Then the residue calculation gives only k0=l0=0 on the RHS, and ∂_{x1}(Q1Q2)=2x1x2^2 is not in the span. The proof sketch contains an algebraic identity that only holds for δ=1. Since Corollary 49, Lemma 53, Lemma 59, and Theorem 44 all depend on this lemma, the paper's headline constant-depth result is currently unproven.\n\nThat's the one serious problem. The rest of the paper deserves credit. The Nullstellensatz degree lower bounds for fully symmetric polynomials of any degree and the vector-invariant instances are genuinely new, and the vector-invariant construction gives the first IPS-fragment lower bounds over finite fields. The barrier theorem (Section 7) is clearly scoped by Definition 64 and is a real limitation of the functional lower bound method. Sections 4 and 5 look carefully argued.\n\nOne more small note: Corollary 49 has a notational slip (residue_k(d_i) should be residue_k(d'_i)), but that's cosmetic compared to Lemma 48.\n\nWhat to do? This deserves a serious referee. The paper is important enough that the non-Section-6 contributions alone would merit publication, but the constant-depth claims are a major advertised result. My recommendation: send to peer review with a clear request to fix or replace Lemma 48 and re-derive Section 6. If it can't be fixed, the paper should be revised to either retract the individual-degree generalization or present it as conditional. I'd cite it for the barrier and the finite-field lower bounds, but not for constant-depth IPS until this is resolved.","headline":"Strong and important paper with a real hole: Section 6's central lemma is false as stated, so the constant-depth individual-degree results are unproven; Sections 3-5 and 7 hold up.","tokens_in":60104,"tokens_out":3898,"would_cite":true,"duration_ms":35649,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Symmetry-based hard instances yield exponential algebraic proof lower bounds and a new barrier for Boolean instances","keywords":["proof complexity","algebraic proof systems","Ideal Proof System","Nullstellensatz","functional lower bound method","symmetric polynomials","vector invariants","roABP-IPS"],"falsifier":"Take a specific unsatisfiable CNF $F=\\{f_i=0\\}$, a polynomial $f$ with no Boolean roots that semantically implies $F$, and a proof system $P$ claimed to be sufficiently strong. If one can exhibit a sequence of instances where either deriving the arithmetization of $\\bigwedge_i f_i$ from $F$ or deriving each $f_i$ from $f=0$ provably requires superpolynomial size, while $1/f$ still has no small circuit in the relevant class, then the barrier theorem's premise fails for that system.","tokens_in":2123,"feed_emoji":"🧮","tokens_out":3422,"duration_ms":98031,"temperature":0.7,"pith_summary":"This paper studies algebraic proof systems in which refuting an unsatisfiable set of polynomial equations means deriving 1 from the equations together with the Boolean axioms $x_i^2 - x_i$. The positive claim is that symmetry, in two forms, produces many new hard instances for fragments of the Ideal Proof System (IPS): Nullstellensatz degree lower bounds, then exponential size lower bounds for refutations written as read-once oblivious algebraic branching programs, and $n^{\\Omega(\\log n)}$ lower bounds for multilinear formula refutations, all over fields of characteristic at least 5, giving the first IPS fragment lower bounds over finite fields. The negative claim is a barrier: the functional lower bound method cannot establish lower bounds for any Boolean instance, such as a CNF, against any sufficiently strong proof system, including $\\mathrm{AC}^0[p]$-Frege and $\\mathrm{TC}^0$-Frege. This matters because these proof systems are the main route so far toward lower bounds for strong propositional proof systems, and the paper delimits exactly where that route stops.","feed_headline":"Symmetry yields proof lower bounds, then a barrier","feed_subtitle":"New hard instances for IPS fragments over finite fields; the functional method cannot reach Boolean CNFs.","key_machinery":"The engine of the positive results is a monomial-counting identity for elementary symmetric polynomials: modulo the Boolean axioms, $e_{d,n}(x)e_{k,n}(x) = 2^{d+k}e_{d+k,n}(x)$ plus lower-degree terms whenever $k \\le n-d$. Iterating this identity shows that any symmetric polynomial of degree $d$ can only be multiplied into 1 by a polynomial of degree at least $n-d+1$; a similar exact coefficient analysis of the degree-2n slice of the reciprocal of the invariant polynomial $Q(x,y)=\\prod_{i\\ \\text{odd}}(x_i y_{i+1}-y_i x_{i+1})-\\beta$ gives the invariant degree lower bound. These degree bounds are lifted to size bounds by substitutions such as $w_{i,j}\\mapsto z_{i,j}x_i x_j$, which embed the original hard instance into a larger one so that evaluation dimension, the dimension of the space of partial Boolean evaluations, is large, forcing large roABP width. The barrier is carried by the identity $1-\\prod_i(1-f_i(x))$, the arithmetic AND of Boolean polynomials, which is 1 on the Boolean cube and hence derivable from Boolean axioms; a sufficiently strong proof system derives this AND efficiently, so any hard $f$ that implies the Boolean instance $F$ yields a small circuit computing $1/f$.","core_discovery":"The paper establishes two complementary statements. Positively, it shows that Nullstellensatz degree lower bounds can be obtained and then lifted to IPS size lower bounds for two families of non-Boolean hard instances: every unsatisfiable symmetric polynomial of degree $d$ requires refutation degree at least $n+1$, and an invariant polynomial $Q(x,y)$ built from $n$ determinants requires degree $2n$; lifting these with gadget substitutions gives exponential roABP-IPSLIN\\' lower bounds and quasipolynomial multilinear-formula-IPS lower bounds, including the first finite-field results for such fragments. Negatively, the functional lower bound method is shown to be powerless for Boolean instances against sufficiently strong proof systems: if a proof system can efficiently derive the arithmetization of the AND of any Boolean polynomials, then any Boolean instance $F$ is refutable from Boolean axioms once a single hard polynomial $f$ implies $F$, so no lower bound against $F$ can follow from hardness of $1/f$.","pith_inferences":["Beyond the paper, the barrier suggests that any candidate for Boolean lower bounds via algebraic proofs must either use a proof system that cannot efficiently derive conjunctions, or use a method other than the single-function $1/f$ reduction.","The exact degree-2n coefficient characterization of the invariant instance points to a family of functional-lower-bound hard functions parameterized by group actions; other vector invariants with sparse high-degree slices may yield further finite-field hard instances.","The tradeoff between depth and individual degree in the constant-depth theorem offers a concrete next test: whether constant-depth refutations of individual degree $\\omega(\\log\\log n)$ can be ruled out for stronger Boolean-like instances, or whether the upper bounds for pigeonhole and Tseitin formulas can be pushed to higher individual degree."],"forward_implications":["Every unsatisfiable symmetric polynomial of degree $O(\\log n)$ can be lifted to an instance with $2^{\\Omega(n)}$ lower bound against roABP-IPSLIN\\' in any variable order.","The invariant instance gives the first IPS fragment lower bounds over finite fields: $\\exp(\\Omega(n))$ for roABP-IPSLIN\\' and $n^{\\Omega(\\log n)}$ for multilinear-formula-IPS.","Constant-depth IPS lower bounds now hold for refutations of individual degree $O(\\log\\log n)$, a strictly stronger model than multilinear constant-depth proofs.","The functional lower bound method cannot prove lower bounds for Boolean instances against $\\mathrm{AC}^0[p]$-Frege, $\\mathrm{TC}^0$-Frege, or constant-depth IPSLIN\\' with Boolean instances, because those systems have AND-introduction.","The open route left is CNF lower bounds against roABP-IPS and multilinear-formula-IPS, which are not sufficiently strong in the barrier sense."],"supporting_citations":[{"why":"Introduces the functional lower bound method, the lifting scheme, and the subset-sum baseline that the paper generalizes.","marker":"[FSTW21]"},{"why":"Defines the Ideal Proof System and shows its simulation of strong propositional proof systems, making the barrier for Boolean instances relevant.","marker":"[GP18]"},{"why":"Supplies the Affine Projections of Partials (APP) framework and residue-based lower bounds used for the constant-depth results.","marker":"[AGK+23]"},{"why":"Proves earlier constant-depth multilinear IPS lower bounds and introduces the knapsack-over-word instance that Section 6 extends.","marker":"[GHT22]"},{"why":"Provides the constant-depth algebraic circuit lower bounds and homogenization transformation used in the lifted-knapsack lower bound.","marker":"[LST21]"},{"why":"Supplies the coefficient-dimension-based multilinear formula lower bounds used for the $n^{\\Omega(\\log n)}$ bound.","marker":"[RY09]"},{"why":"Develops functional lower bounds in algebraic circuit complexity and the evaluation-dimension perspective used throughout the lifting arguments.","marker":"[FKS16]"}],"fun_headline_variants":["Symmetry yields IPS hardness, but Boolean CNFs resist","Algebraic proof lower bounds via symmetry, not for Boolean","New IPS hard instances, finite fields, but no CNF barrier","Symmetry lifts proof complexity, functional method falls short","IPS lower bounds from symmetry, Boolean instances untouched"],"cache_read_input_tokens":62208,"weakest_assumption_plain":"The barrier applies only to proof systems that can efficiently derive the arithmetization of the conjunction of any Boolean polynomials; if a system lacks this AND-introduction power, the construction that produces a small circuit for $1/f$ collapses.","fun_headline_variants_meta":{"raw":{"variants":["Symmetry yields IPS hardness, but Boolean CNFs resist","Algebraic proof lower bounds via symmetry, not for Boolean","New IPS hard instances, finite fields, but no CNF barrier","Symmetry lifts proof complexity, functional method falls short","IPS lower bounds from symmetry, Boolean instances untouched"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000219,"raw_usage":{"total_tokens":1444,"prompt_tokens":945,"completion_tokens":499,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":561,"completion_tokens_details":{"reasoning_tokens":419}},"tokens_in":561,"tokens_out":499,"duration_ms":4697,"temperature":1.0,"reasoning_tokens":419,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T23:33:24.398884+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a specific unsatisfiable CNF $F=\\{f_i=0\\}$, a polynomial $f$ with no Boolean roots that semantically implies $F$, and a proof system $P$ claimed to be sufficiently strong. If one can exhibit a sequence of instances where either deriving the arithmetization of $\\bigwedge_i f_i$ from $F$ or deriving each $f_i$ from $f=0$ provably requires superpolynomial size, while $1/f$ still has no small circuit in the relevant class, then the barrier theorem's premise fails for that system.","supporting_citations":[],"review_version":1}