Pith. sign in

REVIEW 2 major objections 3 minor 50 references

Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

T0 review · 2 major / 3 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Symmetry-based hard instances yield exponential algebraic proof lower bounds and a new barrier for Boolean instances

desk verdict 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. read the letter →

arxiv 2412.20114 v1 pith:QDQQCGDE submitted 2024-12-28 cs.CC

Tuomas Hakoniemi , Nutan Limaye , Iddo Tzameret This is my paper · ORCID
classification cs.CC
keywords proofcomplexityalgebraicsystemsIdealSystemNullstellensatzfunctionallowerboundmethodsymmetricpolynomialsvectorinvariantsroABP-IPS
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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$.

What would settle it

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.

Watch

Extended reading notes

Core claim

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$.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 3 minor

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.

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 (2)
  1. [§3.1, Claim 26 and Eq. (26.1)] 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.
  2. [§6.1.1, Lemma 48] 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.
minor comments (3)
  1. [§6.1.1, Corollary 49] 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.
  2. [§6.1.2, Lemma 51 proof sketch] The displayed formula for α contains a typo: '∑_{ν=0}^{Δ−1} (−1)^nu τ^{2ν−1}' should presumably be '∑_{ν=0}^{Δ−1} (−1)^ν τ^{2^ν−1}'.
  3. [§4.1.2, Proposition 37 and Corollary 38] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular reduction found: the main lower bounds and barrier are proved in-text from explicit computations and published external machinery, and the flagged Lemma 48 gap is a correctness issue, not a circular one.

full rationale

The paper's derivation chain is self-contained rather than circular. The degree bounds (Theorem 32) rest on an explicit coefficient computation (Lemma 30), the size bounds (Theorem 41) are proved via coefficient-dimension arguments on the gadget instance P(u,z) constructed in the paper, and the barrier (Theorem 65) is proved from Definition 64 by a genuine collapse: equations (65.1)-(65.3) exhibit sum_i h_i g_i in C' computing 1/f over the Boolean cube. The definition of 'sufficiently strong' states the AND-introduction hypothesis; it does not assert the conclusion, and the paper explicitly records the escape route (roABP-IPS and multilinear-formula-IPS are not sufficiently strong; CNF lower bounds there remain open, Section 7.1), so no result is equal to its own input by construction. No parameter is fitted and then renamed a prediction; beta is a free constant chosen only for unsatifiability. Self-citations (FSTW21's Theorem 1, GHT22's Claim 58, LST21) point to published peer-reviewed results used as tools; FSTW21 is restated with its proof sketched in-text, and GHT22's Claim 58 is parameter-free and does not encode the target lower bound, so these citations are real evidence under the review rules, not load-bearing circularity. One non-circularity issue is flagged for the record: Lemma 48 (Section 6.1.1) is false as stated. Take t=2, Q_1=x_1^2, Q_2=x_2^2, d'=4, d=2, delta=2, k=1; then residue_1(2,2)=1/2 and the index condition k0+(k/(d-k))·ell0 <= k - residue/delta = 3/4 forces k0=ell0=0, so the right-hand side is span{1, x_1^2, x_2^2, x_1^2·x_2^2}, which does not contain partial_{x_1}(Q_1·Q_2)=2·x_1·x_2^2. The proof sketch's identity sum_i (|kappa_i| - (k/(d-k))·(d'_i - |kappa_i|)) = sum_i (delta·d/(d-k))·(|kappa_i| - (k/(delta·d))·d'_i) holds only for delta=1. Corollary 49, Lemmas 53 and 59, and Theorem 44 depend on Lemma 48, so the bounded-individual-degree constant-depth bounds are unproven as written. This is a correctness gap, not a circular reduction; the overall verdict is no significant circularity.

Assumptions & free parameters 0 free parameters · 8 assumptions · 0 invented entities

The central results are mathematical theorems resting on standard theorems in algebraic complexity and proof complexity, plus explicit field-characteristic assumptions. No free parameters are fitted to data; beta is a universally quantified scalar chosen outside a forbidden set. No invented physical entities are introduced.

assumptions (8)
  • standard math Fundamental theorem of symmetric polynomials (Proposition 6)
    Used to decompose symmetric polynomials as polynomials in elementary symmetric polynomials in Corollary 27.
  • standard math Hilbert Nullstellensatz over polynomial ideals
    Underlies the definition of Nullstellensatz and IPS refutations in Definitions 7 and 8.
  • standard math Nisan's coefficient matrix rank lemma (Lemma 14)
    Converts coefficient dimension lower bounds into roABP width lower bounds in Theorems 35, 39, and 41.
  • standard math Raz-Yehudayoff multilinear formula lower bounds (Theorem 20)
    Gives multilinear formula and product-depth multilinear formula lower bounds for the lifted invariant instance in Theorem 41.
  • standard math AGK+23 APP framework lemmas (Lemmas 46, 47, 50, 52)
    The constant-depth lower bounds in Section 6 adapt these lemmas to bounded individual degree; the paper provides proof sketches for the adapted versions.
  • standard math Functional lower bound method (Theorem 1 from FSTW21)
    Core reduction used throughout, from hardness of computing 1/f over the Boolean cube to IPS lower bounds.
  • domain assumption Field characteristic restrictions: char(F) >= 5 or char(F) = 0 or char(F) > max(2n, nd)
    Keeps coefficients such as 2^(d+k) nonzero and ensures beta can be chosen outside forbidden values; limits the scope of the results.
  • domain assumption Sufficiently strong proof system condition (Definition 64)
    The barrier theorem applies only to proof systems that can efficiently derive the arithmetization of conjunctions, such as AC0[p]-Frege, TC0-Frege, and constant-depth IPSLIN'.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers." pith.science (2026). https://pith.science/paper/QDQQCGDE

@misc{pith2026241220114,
  author       = {Pith},
  title        = {Pith review of: Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QDQQCGDE}},
  note         = {Machine review of arXiv:2412.20114}
}
read the original abstract

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi [GP18]) 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]), 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

50 extracted references · 22 canonical work pages

  1. [1]

    Robert Andrews and Michael A. Forbes. Ideals, determinants, and straightening: proving and using lower bounds for polynomial ideals. In Proceedings of the 54th Annual ACM SIGACT Symposium on Theory of Computing , STOC 2022, page 389–402, New York, NY, USA, 2022. Association for Computing Machinery. Available from: https://doi.org/10.1145/3519935.3520025, ...

    arXiv 2022

  2. [3]

    Low-Depth Arithmetic Circuit Lower Bounds: Bypassing Set-Multilinearization

    Prashanth Amireddy, Ankit Garg, Neeraj Kayal, Chandan Saha, and Bhargav Thankey. Low-Depth Arithmetic Circuit Lower Bounds: Bypassing Set-Multilinearization . In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) , volume 261 of Leibniz International Proceedings in...

    2023

  3. [4]

    The complexity of the pigeonhole principle

    Mikl\' o s Ajtai. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science , pages 346--355, 1988

    work page 1988

  4. [5]

    A Lower Bound for Polynomial Calculus with Extension Rule

    Yaroslav Alekseev. A Lower Bound for Polynomial Calculus with Extension Rule . In Valentine Kabanets, editor, 36th Computational Complexity Conference (CCC 2021) , volume 200 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 21:1--21:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik. Available from: htt...

    work page doi:10.4230/lipics.ccc.2021 2021

  5. [6]

    Lower bounds on H ilbert's N ullstellensatz and propositional proofs

    Paul Beame, Russell Impagliazzo, Jan Kraj \' c ek, Toniann Pitassi, and Pavel Pudl \'a k. Lower bounds on H ilbert's N ullstellensatz and propositional proofs. Proc. London Math. Soc. (3) , 73(1):1--26, 1996. http://dx.doi.org/10.1112/plms/s3-73.1.1 doi:10.1112/plms/s3-73.1.1

    doi:10.1112/plms/s3-73.1.1 1996

  6. [7]

    Buss, Russell Impagliazzo, Jan Kraj \' c ek, Pavel Pudl \' a k, Alexander A

    Samuel R. Buss, Russell Impagliazzo, Jan Kraj \' c ek, Pavel Pudl \' a k, Alexander A. Razborov, and Ji r \' Sgall. Proof complexity in algebraic systems and bounded depth F rege systems with modular counting. Computational Complexity , 6(3):256--298, 1996. http://dx.doi.org/10.1007/BF01294258 doi:10.1007/BF01294258

    doi:10.1007/bf01294258 1996

  7. [8]

    Lower bounds for cutting planes proofs with small coefficients

    Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. The Journal of Symbolic Logic , 62(3):708--728, 1997. Available from: https://doi.org/10.2307/2275569

    work page doi:10.2307/2275569 1997

  8. [9]

    Campbell and I.P

    H.E.A. Campbell and I.P. Hughes. Vector invariants ofu2(fp) : A proof of a conjecture of richman. Advances in Mathematics , 126(1):1--20, 1997. Available from: https://www.sciencedirect.com/science/article/pii/S000187089691590X, http://dx.doi.org/https://doi.org/10.1006/aima.1996.1590 doi:https://doi.org/10.1006/aima.1996.1590

    work page arXiv 1997

Show all 50 references
  1. [10]

    Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra

    David Cox, John Little, and Donal O'Shea. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra . Undergraduate Texts in Mathematics. Springer Cham, fourth edition, 2015. http://dx.doi.org/10.1007/978-3-319-16721-3 doi:1...

    2015 doi

  2. [11]

    Computational Invariant Theory , volume 130 of Encyclopaedia of Mathematical Sciences

    Harm Derksen and Gregor Kemper. Computational Invariant Theory , volume 130 of Encyclopaedia of Mathematical Sciences . Springer, Berlin, Heidelberg, 2 edition, 2015. http://dx.doi.org/10.1007/978-3-662-48422-7 doi:10.1007/978-3-662-48422-7

    2015 doi

  3. [12]

    New lower bounds for polynomial calculus over non-boolean bases

    Yogesh Dahiya, Meena Mahajan, and Sasank Mouli. New lower bounds for polynomial calculus over non-boolean bases. Electron. Colloquium Comput. Complex. , TR23-132 , 2023. Available from: https://eccc.weizmann.ac.il/report/2023/132, http://arxiv.org/abs/TR23-132 arXiv:TR23-132

    2023

  4. [13]

    de Rezende, Mika G \" o \" o s, and Robert Robere

    Susanna F. de Rezende, Mika G \" o \" o s, and Robert Robere. Guest column: Proofs, circuits, and communication. SIGACT News , 53(1):59--82, 2022. Available from: https://doi.org/10.1145/3532737.3532746, http://dx.doi.org/10.1145/3532737.3532746 doi:10.1145/3532737.3532746

    2022

  5. [14]

    Forbes, Mrinal Kumar, and Ramprasad Saptharishi

    Michael A. Forbes, Mrinal Kumar, and Ramprasad Saptharishi. Functional Lower Bounds for Arithmetic Circuits and Connections to Boolean Circuit Complexity . In Ran Raz, editor, 31st Conference on Computational Complexity (CCC 2016) , volume 50 of Leibniz International Proceedin...

    2016 doi

  6. [15]

    Michael A. Forbes. Polynomial Identity Testing of Read-Once Oblivious Algebraic Branching Programs . PhD thesis, Massachusetts Institute of Technology, June 2014. Available from: http://hdl.handle.net/1721.1/89843

    2014

  7. [16]

    Forbes and Amir Shpilka

    Michael A. Forbes and Amir Shpilka. Quasipolynomial-time identity testing of non-commutative and read-once oblivious algebraic branching programs. In 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, 26-29 October, 2013, Berkeley, CA, USA , pages 243--2...

    2013 doi

  8. [17]

    Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson

    Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof complexity lower bounds from algebraic circuit complexity. Theory Comput. , 17:1--88, 2021. Available from: https://theoryofcomputing.org/articles/v017a010/

    2021

  9. [18]

    Dima Grigoriev and Edward A. Hirsch. Algebraic proof systems over formulas. Theoretical Computer Science , 303(1):83--102, 2003. Available from: https://www.sciencedirect.com/science/article/pii/S0304397502004462, http://dx.doi.org/https://doi.org/10.1016/S0304-3975(02)00446-2...

    2003 doi

  10. [19]

    Simple hard instances for low-depth algebraic proofs

    Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022 , pages 188--199. IEEE , 2022. Available ...

    2022

  11. [20]

    Learning sums of powers of low-degree polynomials in the non-degenerate case

    Ankit Garg, Neeraj Kayal, and Chandan Saha. Learning sums of powers of low-degree polynomials in the non-degenerate case. In Sandy Irani, editor, 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020 , pages 889--899. I...

    2020

  12. [21]

    Grochow and Toniann Pitassi

    Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM , 65(6):37:1--37:59, 2018. Available from: https://doi.org/10.1145/3230742, http://dx.doi.org/10.1145/3230742 doi:10.1145/3230742

    2018 doi

  13. [22]

    T seitin's tautologies and lower bounds for N ullstellensatz proofs

    Dima Grigoriev. T seitin's tautologies and lower bounds for N ullstellensatz proofs. In IEEE Symposium on Foundations of Computer Science , pages 648--652, 1998. http://dx.doi.org/10.1109/SFCS.1998.743515 doi:10.1109/SFCS.1998.743515

    1998

  14. [23]

    Joshua A. Grochow. Polynomial identity testing and the ideal proof system: PIT is in NP if and only if IPS can be p-simulated by a cook-reckhow proof system. CoRR , abs/2306.02184, 2023. Available from: https://doi.org/10.48550/arXiv.2306.02184, http://arxiv.org/abs/2306.02184...

    2023 doi arXiv

  15. [24]

    Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields

    Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields . In Amnon Ta-Shma, editor, 38th Computational Complexity Conference (CCC 2023) , volume 264 of Leibniz International Proceedings in Informa...

    2023 doi

  16. [25]

    Lower bounds for the polynomial calculus and the G r \" o bner basis algorithm

    Russell Impagliazzo, Pavel Pudl \' a k, and Ji r \' Sgall. Lower bounds for the polynomial calculus and the G r \" o bner basis algorithm. Computational Complexity , 8(2):127--144, 1999. http://dx.doi.org/10.1007/s000370050024 doi:10.1007/s000370050024

    1999 doi

  17. [26]

    IPS -like proof systems based on binary decision diagrams

    Alexander Knop. IPS -like proof systems based on binary decision diagrams. Electron. Colloquium Comput. Complex. , TR17-179 , 2017. Available from: https://eccc.weizmann.ac.il/report/2017/179, http://arxiv.org/abs/TR17-179 arXiv:TR17-179

    2017

  18. [27]

    An exponential lower bound to the size of bounded depth F rege proofs of the pigeonhole principle

    Jan Kraj \' c ek, Pavel Pudl \'a k, and Alan Woods. An exponential lower bound to the size of bounded depth F rege proofs of the pigeonhole principle. Random Structures & Algorithms , 7(1):15--39, 1995. Available from: https://doi.org/10.1002/rsa.3240070103

    1995 doi

  19. [28]

    Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic

    Jan Kraj \' c ek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic , 62(2):457--486, 1997. Available from: https://doi.org/10.2307/2275541

    1997 doi

  20. [29]

    Superpolynomial lower bounds against low-depth algebraic circuits

    Nutan Limaye, Srikanth Srinivasan, and S \' e bastien Tavenas. Superpolynomial lower bounds against low-depth algebraic circuits. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022 , pages 804--814. IEEE , 2021. Av...

    2021

  21. [30]

    Characterizing propositional proofs as noncommutative formulas

    Fu Li, Iddo Tzameret, and Zhengyu Wang. Characterizing propositional proofs as noncommutative formulas. In SIAM Journal on Computing , volume 47, pages 1424--1462, 2018. Full Version: http://arxiv.org/abs/1412.8746

    2018 arXiv

  22. [31]

    Lower bounds for non-commutative computation

    Noam Nisan. Lower bounds for non-commutative computation. In Proceedings of the Annual ACM Symposium on the Theory of Computing 1991 , pages 410--418, 1991. http://dx.doi.org/10.1145/103418.103462 doi:10.1145/103418.103462

    1991

  23. [32]

    Exponential lower bounds for the pigeonhole principle

    Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. computational complexity , 3(2):97--140, 1993. Available from: https://doi.org/10.1007/BF01200117, http://dx.doi.org/10.1007/BF01200117 doi:10.1007/BF01200117

    1993 doi

  24. [33]

    Algebraic propositional proof systems

    Toniann Pitassi. Algebraic propositional proof systems. In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop 1996, Princeton, New Jersey, USA, January 14-17, 1996 , volume 31 of DIMACS Series in Discrete ...

    1996 doi

  25. [34]

    Unsolvable systems of equations and proof complexity

    Toniann Pitassi. Unsolvable systems of equations and proof complexity. In Proceedings of the International Congress of Mathematicians, Berlin, 1998 , volume Extra Vol. ICM Berlin 1998, Vol. III, pages 451--460, 1998. http://dx.doi.org/10.4171/DMS/1-3/44 doi:10.4171/DMS/1-3/44

    1998 doi

  26. [35]

    Algebraic proof complexity: Progress, frontiers and challenges

    Tonnian Pitassi and Iddo Tzameret. Algebraic proof complexity: Progress, frontiers and challenges. ACM SIGLOG News , 3(3), 2016

    2016

  27. [36]

    Razborov

    Alexander A. Razborov. Lower bounds for the polynomial calculus. Comput. Complexity , 7(4):291--324, 1998

    1998

  28. [37]

    Separation of multilinear circuit and formula size

    Ran Raz. Separation of multilinear circuit and formula size. Theory of Computing , 2(6):121--135, 2006. Preliminary version appeared in IEEE Annual Symposium on Foundations of Computer Science 2004 . http://dx.doi.org/10.4086/toc.2006.v002a006 doi:10.4086/toc.2006.v002a006

    2006 doi

  29. [38]

    Multi-linear formulas for permanent and determinant are of super-polynomial size

    Ran Raz. Multi-linear formulas for permanent and determinant are of super-polynomial size. J. ACM , 56(2), 2009. Preliminary version appeared in Proceedings of the Annual ACM Symposium on the Theory of Computing 2004 . http://dx.doi.org/10.1145/1502793.1502797 doi:10.1145/1502...

    2009

  30. [39]

    On vector invariants over finite fields

    David R Richman. On vector invariants over finite fields. Advances in Mathematics , 81(1):30--65, 1990. Available from: https://www.sciencedirect.com/science/article/pii/0001870890900036, http://dx.doi.org/https://doi.org/10.1016/0001-8708(90)90003-6 doi:https://doi.org/10.101...

    1990

  31. [40]

    Resolution over linear equations and multilinear proofs

    Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic , 155(3):194--224, 2008. Available from: http://dx.doi.org/10.1016/j.apal.2008.04.001, http://dx.doi.org/10.1016/j.apal.2008.04.001 doi:10.1016/j.apal.2008.04.001

    2008 doi

  32. [41]

    The strength of multilinear proofs

    Ran Raz and Iddo Tzameret. The strength of multilinear proofs. Computational Complexity , 17(3):407--457, 2008. Available from: http://dx.doi.org/10.1007/s00037-008-0246-0, http://dx.doi.org/10.1007/s00037-008-0246-0 doi:10.1007/s00037-008-0246-0

    2008 doi

  33. [42]

    Balancing syntactically multilinear arithmetic circuits

    Ran Raz and Amir Yehudayoff. Balancing syntactically multilinear arithmetic circuits. Computational Complexity , 17(4):515--535, 2008. http://dx.doi.org/10.1007/s00037-008-0254-0 doi:10.1007/s00037-008-0254-0

    2008 doi

  34. [43]

    Lower bounds and separations for constant depth multilinear circuits

    Ran Raz and Amir Yehudayoff. Lower bounds and separations for constant depth multilinear circuits. Computational Complexity , 18(2):171--207, 2009. Preliminary version appeared in IEEE Conference on Computational Complexity CCC 2008 . http://dx.doi.org/10.1007/s00037-009-0270-...

    2009 doi

  35. [44]

    Personal communication to Forbes-Shpilka ForbesShpilka13b

    Ramprasad Saptharishi, 2012. Personal communication to Forbes-Shpilka ForbesShpilka13b

    2012

  36. [45]

    A survey of lower bounds in arithmetic circuit complexity, 2016-2022

    Ramprasad Saptharishi. A survey of lower bounds in arithmetic circuit complexity, 2016-2022. Available from: https://github.com/dasarpmar/lowerbounds-survey/releases

    2016

  37. [46]

    Diagonal circuit identity testing and lower bounds

    Nitin Saxena. Diagonal circuit identity testing and lower bounds. In ICALP 2008 , pages 60--71, 2008. ECCC 07 124 . http://dx.doi.org/10.1007/978-3-540-70575-8_6 doi:10.1007/978-3-540-70575-8_6

    2008 doi

  38. [47]

    (semi)algebraic proofs over \( \) 1 variables

    Dmitry Sokolov. (semi)algebraic proofs over \( \) 1 variables. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 2...

    2020

  39. [48]

    Iterated lower bound formulas: a diagonalization-based approach to proof complexity

    Rahul Santhanam and Iddo Tzameret. Iterated lower bound formulas: a diagonalization-based approach to proof complexity. In Samir Khuller and Virginia Vassilevska Williams, editors, STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing, Virtual Event, Italy, June 21...

    2021

  40. [49]

    Depth-3 arithmetic circuits over fields of characteristic zero

    Amir Shpilka and Avi Wigderson. Depth-3 arithmetic circuits over fields of characteristic zero. Comput. Complexity , 10:1--27, 2001

    2001

  41. [50]

    Arithmetic circuits: A survey of recent results and open questions

    Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Foundations and Trends in Theoretical Computer Science , 5(3-4):207--388, 2010

    2010

  42. [51]

    Algebraic proofs over noncommutative formulas

    Iddo Tzameret. Algebraic proofs over noncommutative formulas. Inf. Comput. , 209(10):1269--1292, 2011. Available from: http://dx.doi.org/10.1016/j.ic.2011.07.004, http://dx.doi.org/10.1016/j.ic.2011.07.004 doi:10.1016/j.ic.2011.07.004

    2011 doi

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.