Lower Bounds against the Ideal Proof System in Finite Fields

Iddo Tzameret; Jiaqi Lu; Nashlen Govindasamy; Tal Elbaz

REVIEW 4 major objections 5 minor 17 references

Lower Bounds against the Ideal Proof System in Finite Fields

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read This paper proves that no polynomial-size constant-depth multilinear Ideal Proof System refutation of a knapsack-mod-p polynomial exists over any fixed finite field of characteristic at least 5.

desk verdict Real progress on IPS over finite fields, but the main lower bound currently rests on a false corollary and an unproved balanced-word construction; salvageable, not there yet. read the letter →

arxiv 2506.17210 v1 pith:HFD3TTJK submitted 2025-06-20 cs.CC

Tal Elbaz , Nashlen Govindasamy , Jiaqi Lu , Iddo Tzameret This is my paper · ORCID

classification cs.CC MSC 03F2068Q1768Q15

keywords algebraicproofcomplexityIdealSystemfinitefieldsAC0[p]-Fregeconstant-depthcircuitsknapsackpolynomialset-multilinearread-onceobliviousbranchingprograms

topics P versus NP

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 proves lower bounds for the Ideal Proof System (IPS), an algebraic proof system in which a refutation is a single algebraic circuit witnessing that 1 lies in the ideal generated by a set of polynomial equations over a field. Earlier IPS lower bounds were proved only over large or characteristic-zero fields, while finite fields are the natural setting for proving lower bounds for propositional proof systems such as $AC^{0}$[p]-Frege. The central result is that a knapsack-mod-p polynomial, a variant of a previously studied subset-sum-style instance, has no polynomial-size constant-depth multilinear IPS_LIN' refutation over any field of characteristic p>=5. The paper also separates this finite-field proof system from the characteristic-zero one, proves exponential lower bounds for read-once algebraic branching program refutations over finite fields, and shows that any lower bound for a non-multilinear constant-depth IPS instance over a finite field would produce a hard CNF formula and hence an $AC^{0}$[p]-Frege lower bound.

What carries the argument

The load-bearing object is the knapsack-mod-p polynomial $\mathrm{ks}_{w,p}$, together with the relative rank of the coefficient matrix of its reciprocal—that is, the rank divided by the square root of the product of the row and column counts. The word $w$ must be balanced, meaning every index has at least one overlap with an index of the opposite sign, and must admit a scattered partition of its positive indices into fewer than p parts; these conditions make the embedded p-1 powers Boolean functions and let the instance be shifted to an unsatisfiable one. The argument's engine is a rank lower bound (Lemma 21): for the multilinear polynomial $f$ that agrees with $1/\mathrm{ks}_{w,p}$ on Boolean assignments, the matrix $M_w(f)$ has full rank, by an induction on submonomials of the negative variables. Full rank feeds through the set-multilinearization result [For24] and the improved set-multilinear-to-rank bound [BDS24], and the final size lower bound follows; the carrying identity is the full-degree lemma, which says that a multilinear polynomial inverse of a sum of full-degree Boolean functions minus a constant must itself have full degree.

What would settle it

Exhibit a balanced word $w$ over $\{\alpha k,-k\}$ in the parameter range of Theorem 24 whose positive positions cannot be partitioned into fewer than $p$ groups with pairwise disjoint overlaps; that single example would break the construction of $\mathrm{ks}_{w,p}$ and the rank lower bound. Alternatively, for a fixed such word, compute the minimal size of a product-depth-$\Delta$ set-multilinear circuit computing the projection $\Pi_w(1/\mathrm{ks}_{w,p})$: a polynomial-size circuit in $n$ would disprove Lemma 26.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 24: for every prime p>=5 and every field F of characteristic p, any product-depth at most $\Delta$ multilinear $\mathrm{IPS}_{\mathrm{LIN}}'$ refutation over F of the knapsack-mod-p instance $\mathrm{ks}_{w,p}$ has size at least $n^{\Omega(\lambda/\Delta)}$, where $\Delta \le \log\log\log n / 4$ and $\lambda = \lfloor d^{1/G(\Delta)} \rfloor$ with $d = \lfloor \log n / 4 \rfloor$. The hard instance $\mathrm{ks}_{w,p}$ is built from a balanced integer word $w$ over the two-symbol alphabet $\{\alpha k, -k\}$, with a scattered partition of its positive indices into fewer than p parts, and with each summand raised to the p-1 power so that Fermat's little theorem forces it to be Boolean-valued; a suitable shift $\beta$ then makes the whole polynomial unsatisfiable over Boolean assignments. The lower-bound argument reduces refutation size to a full-rank statement about the coefficient matrix of the reciprocal function $1/\mathrm{ks}_{w,p}$ over Boolean assignments, and then rules out small set-multilinear circuits for that projection using a set-multilinearization theorem that works over all fields [For24] together with improved rank-to-size parameters [BDS24]. The paper also proves a separation (Theorem 36): the degree-2 symmetric knapsack $\mathrm{ks}_{w,e2}$ has polynomial-size constant-depth multilinear $\mathrm{IPS}_{\mathrm{LIN}}'$ refutations over any field of characteristic p>=3, but requires super-polynomial size over every characteristic-zero field.

Load-bearing premise

The weakest load-bearing premise is a one-sentence assertion in the proof of Theorem 24 that a balanced integer word $w$ over $\{\alpha k,-k\}$ with exactly $d$ positions and with its positive positions partitionable into fewer than $p$ disjoint groups exists; the construction is not given, and if no such word exists for the stated parameters the rank lower bound, and with it the finite-field lower bound, would not go through.

Editorial extensions

If this is right

For every fixed prime p>=5, the knapsack-mod-p polynomial is a concrete super-polynomial hard instance for constant-depth multilinear $\mathrm{IPS}_{\mathrm{LIN}}'$ over all fields of characteristic p.
The same instance also stays hard over characteristic-zero fields, so it supplies new hard instances for the earlier characteristic-zero proof system as well.
The degree-2 symmetric knapsack separates the two settings: it has short constant-depth multilinear refutations over fields of characteristic at least 3, but all such refutations over characteristic-zero fields require super-polynomial size.
Over any fixed finite field, explicit instances force any roABP-$\mathrm{IPS}_{\mathrm{LIN}}'$ refutation, in any variable order, to have exponential size; the paper also shows the functional lower bound method alone cannot produce non-placeholder versions of these bounds over finite fields.
If any instance is shown hard for non-multilinear bounded-depth IPS over a finite field, the translation lemma converts it into a hard CNF and hence, by known simulations, into an AC^0[p]-Frege lower bound.

Reading between the lines

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

Beyond the paper: the unproved balanced-word existence claim, if it fails for some parameters, would not necessarily destroy the whole lower-bound method; a different word family or a different scattered partition might restore the rank argument, and testing the construction explicitly for small d and k is a cheap way to check the route.
Beyond the paper: the translation lemma's removal of extension axioms suggests that any proof system that can internally derive the finite-field axioms and Lagrange interpolation identities can convert algebraic-instance lower bounds into propositional ones; it would be natural to see whether the same internal bit-arithmetic works for polynomial calculus or Nullstellensatz fragments over finite fi
Beyond the paper: the separation instance $\mathrm{ks}_{w,e2}$ shows that the characteristic of the field can change the complexity of the same algebraic instance; one could look for a family whose required refutation size varies with p, giving a finer map of how IPS strength depends on the ground field.
Beyond the paper: the paper's limitation statement for roABP-IPS means that non-placeholder roABP-IPS lower bounds over finite fields would need a method that is not the functional lower bound method; lower-bound-by-multiples is the natural candidate, but it has not yet been pushed to non-placeholder instances in this setting.

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.

Desk Editor's Note

read the letter

Colleague,

Here's my read of arXiv:2506.17210. The headline result — super-polynomial lower bounds for constant-depth multilinear IPS_LIN' over fixed finite fields — is not established as written. The gap is concrete: Corollary 23 asserts that a balanced word with |w_i|≤b satisfies |w_P|-|w_N|≥-b, but an alternating word (+αk,-k,+αk,-k,...) is balanced and has |w_P|-|w_N|=(α-1)k·d/2, which for large d is far below -b. So the relative-rank lower bound 2^{-b/2} does not follow from balance alone. The proof of Theorem 24 then says 'Construct, by induction, a balanced word w∈Z^d over the alphabet {αk,-k}' without giving the construction or the extra condition (essentially |w_N|≤|w_P|+k and Δ_G(N_w)≤3) that would make Corollary 23 true. That is load-bearing: Lemma 26 depends on it.

That said, there is real substance here. The knapsack-mod-p instance is a new construction, and the degree lemma (Lemma 19) plus the rank argument (Lemma 21) are spelled out carefully. The separation result (Theorem 36) — using the symmetric knapsack of degree 2 and Fermat's little theorem for the upper bound — is a nice idea, though its proof relies on Lemma 35 which is omitted ('essentially the same'). The roABP sections look solid: the hard instance f=∏(1-x_i)-2 is a genuine simplification over HLT24, and the multiples-method proof for the system (f,g,x²-x) is clean. The translation lemma (Section 6) is a genuine contribution: it removes extension axioms from ST25 and gives a direct route from algebraic-instance lower bounds to CNF lower bounds, with the caveat that it does not apply to the paper's own multilinear lower bound, a point the authors acknowledge. There is also a minor exponent discrepancy in Lemma 26, easy to fix.

Bottom line: this paper deserves a serious referee, but the referee should demand a proof of the balanced-word construction or a revised statement, and a corrected Corollary 23, before the main theorem is trusted. The roABP and translation results may stand independently. I would cite the translation lemma, and I would bring it to a reading group to discuss the gap.

Referee Report

4 major / 5 minor

Summary. The paper studies lower bounds for fragments of the Ideal Proof System over finite fields. The central results claimed are: (1) a super-polynomial lower bound for constant-depth multilinear IPS_LIN' refutations of a knapsack mod p instance over any field of fixed characteristic p≥5 (Theorem 24); (2) a separation of this system over finite fields from the characteristic-zero system via a symmetric knapsack instance (Theorem 36); (3) exponential lower bounds for roABP-IPS_LIN' over finite fields, in both fixed and arbitrary variable orders (Theorems 43 and 46), together with a limitation of the functional method (Theorem 49); and (4) a translation lemma showing that algebraic-instance lower bounds against bounded-depth IPS over finite fields imply CNF lower bounds and hence AC^0[p]-Frege lower bounds (Theorem 60). The proofs combine the functional lower bound method, Forbes's set-multilinearization over all fields, the BDS24 rank parameters, and the GHT22 framework.

Significance. If the missing pieces are supplied, these are substantial results: they would give the first lower bounds for constant-depth multilinear IPS over any fixed finite field, removing the large-characteristic assumption that underpins earlier work, and the roABP results give simple finite-field analogues of previous large-field bounds. The translation lemma is a clean conceptual contribution that removes the extension axioms from the earlier ST25 translation. The paper proves several key technical lemmas in detail (Lemma 19, Lemma 21, Lemma 33) and correctly exploits Forbes's set-multilinearization result and the BDS24 improved parameters. However, two load-bearing proofs are only sketched or omitted (the balanced-word construction inside Theorem 24, and Lemma 35), and there is an exponent mismatch in Lemma 26, so the manuscript is not yet in a publishable state.

major comments (4)

[§3.5, proof of Theorem 24] The proof contains the sentence 'Construct, by induction, a balanced word w in Z^d over the alphabet {αk,-k}' but gives neither the construction nor a reference to a lemma establishing it. This is load-bearing: Lemma 26 needs a balanced word with those block lengths, Corollary 23 needs the resulting balance to imply |w_P|-|w_N| ≥ -b, and the scattered partition in the comment after Theorem 24 needs Δ_G(N_w)≤3. Please provide an explicit inductive construction with these parameters, or identify the exact lemma in [GHT22]/[BDS24] and verify that its parameters match d=⌊log n/4⌋ and the stated ranges of α and k.
[§4.2, Lemma 35] The proof of Lemma 35 is omitted ('essentially the same as the proof of Theorem 24 ... and is omitted here'). Since the degree lower bound Lemma 33 is structurally different from the knapsack-mod-p degree argument, and since Theorem 36 is the paper's separation claim, the reduction needs to be written out. At minimum, specify which parts of the Theorem 24 proof carry over verbatim and where Lemma 33 is invoked.
[§3.5, Lemma 26] The inequality chain in the proof gives 2^{-k} ≤ rel-rank(F) ≤ s 2^Δ 2^{-kλ/256}, which yields s ≥ 2^{k(λ/256-1)-Δ}, not the stated s ≥ 2^{k(λ/256-1)/(2Δ)}. The discrepancy should be corrected or explained; as written, the statement of Lemma 26 does not follow from its proof.
[§3.4, Corollary 23] The implication 'w is balanced and |w_i|≤b implies |w_P|-|w_N| ≥ -b' is asserted without proof. It is true under the contiguous-interval interpretation of A(i)_w and B(j)_w (the negative intervals partition [1,|w_N|], so |w_N|>|w_P|+b would leave the last negative interval disjoint from all positive intervals), but the argument should be included, since this inequality is what converts full rank into the relative-rank bound rel-rank ≥ 2^{-b/2}.

minor comments (5)

[Throughout §3 and §4] Several lemmas are cited as 'Theorem 18', 'Theorem 19', 'Theorem 20', and 'Theorem 33'; these cross-references should be changed to 'Lemma'.
[§5.4] The word 'acheive' should be 'achieve'.
[§5.2, Corollary 43] The phrase 'constant characteristics q' should be 'constant characteristic q'.
[§6, Theorem 59] The notation SCNF(C(x)) is used in the proof where Definition 58 writes SCNF(C(x)=0); please make the notation uniform.
[§3.5, Lemma 28] The quoted set-multilinearization bound poly(s, Θ(d/ln d)^d) would benefit from an explicit statement of the dependence of implicit constants on the field, because Theorem 24 later converts this bound into a concrete n^{Ω(λ/Δ)} lower bound.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the finite-field knapsack lower bound rests on new instance analysis and external published lemmas; the load-bearing balanced-word construction is a correctness gap, not a definitional reduction.

full rationale

I walked the main derivation chain: Theorem 24 reduces to Theorem 25, which reduces to Lemma 26, which uses Lemma 21/Corollary 23 for a full-rank/relative-rank lower bound on M_w(f), and Lemma 19/20 for the degree lower bound. These rank and degree statements are proved in the paper, not assumed as the target result. The external inputs, Forbes' set-multilinearization over all fields (Lemma 28) and the BDS24/LST21 relative-rank bound (Claim 27), are published results with independent derivations, so citing them is genuine support under the hard rules. The hard instance ks_{w,p} differs from the GHT22 knapsack by the Fermat power (p-1), and the paper explicitly addresses the finite-field obstacle that the knapsack is Boolean-satisfiable; this is a real modification rather than a renaming. The self-citations to GHT22 and ST25 are present, but the finite-field proofs are re-derived internally and the translation lemma in Section 6 eliminates extension axioms with new Lagrange-polynomial arguments, so the central claims do not reduce by construction to those papers. Separately, I flag a non-circular correctness gap: the proof of Theorem 24 contains only 'Construct, by induction, a balanced word w in Z^d over the alphabet {alpha k, -k}', without giving the induction, and Corollary 23's assertion that balance plus |w_i| <= b implies |w_P|-|w_N| >= -b is unsupported and appears false for balanced alternating words with alpha = 1/2 and large d. This is an omitted proof / unsupported inequality affecting whether Lemma 26's hypotheses are met; it is a correctness risk, not a circular derivation, so the circularity score remains 1.

Assumptions & free parameters 4 free parameters · 9 assumptions · 4 invented entities

The central claims rest on standard algebra (Nullstellensatz, Fermat, Lucas) and on deep published circuit-complexity theorems (Forbes set-multilinearization, BDS24 relative rank, FSTW21 functional method and ABP lower bounds, ST25 translation lemma). The paper's own contribution is the finite-field knapsack instance, the associated rank and degree lemmas, and the removal of extension axioms. The beta parameters and the alpha/k word parameters are construction choices, not fits to the lower-bound statements.

free parameters (4)

beta (knapsack mod p) = an element of F not in {0,...,r}
Chosen so that ks_{w,p} is unsatisfiable over Boolean assignments; existence follows from Fermat's little theorem and r < p. This is a construction parameter of the hard instance, not fitted to the lower bound.
beta (symmetric knapsack) = an element of F such that e_2(x)-beta is unsatisfiable
Existence follows from Lucas's theorem (Lemma 31) when a digit d_i >= 2 appears in the base-p expansion. Again a construction parameter, not fitted to the lower bound.
constant 2 in roABP hard instance f = prod(1-x_i) - 2 = 2
Chosen because q > 2 ensures f has no Boolean root; not fitted to the result.
alpha and k (word parameters) = alpha in [1/2,1), k in [floor(log n)/2, floor(log n)], alpha*k integer
Existential parameters from BDS24/LST21 used to construct the balanced word; they are chosen to make the relative-rank argument work, not fitted to data.

assumptions (9)

standard math Hilbert Nullstellensatz over finite fields
Used to define the Ideal Proof System and to guarantee completeness of the refutation format.
standard math Fermat's little theorem
Used in the construction of ks_{w,p} and in the upper-bound refutations in the separation theorem.
standard math Lucas's theorem
Used in Lemma 31 to show that elementary symmetric sums are unsatisfiable over finite fields.
domain assumption Forbes set-multilinearization over any field (Lemma 28, [For24])
Load-bearing external result that converts constant-depth circuits to constant-depth set-multilinear circuits over any field. This is the key enabler for the finite-field extension.
domain assumption BDS24/LST21 relative-rank bound (Claim 27, [BDS24] Lemma 4.3)
Provides the size lower bound for set-multilinear formulas in terms of relative rank; used in the proof of Lemma 26.
domain assumption FSTW21 full-degree bound for subset-sum (Lemma 18, [FSTW21] Proposition 5.3)
Basis for the generalized degree bound Lemma 19, which is central to the rank lower bound.
domain assumption FSTW21 functional lower bound method (Theorem 10)
Reduces IPS lower bounds to circuit lower bounds for 1/f over Boolean assignments; used throughout the paper.
domain assumption FSTW21 read-twice oblivious ABP lower bound (Lemma 44)
Used in the multiples-method roABP-IPS lower bound over finite fields.
domain assumption ST25 translation lemma for extended CNFs (Lemma 56)
Starting point of Section 6; the paper removes the extension axioms from this lemma.

invented entities (4)

ks_{w,p} (knapsack mod p)
purpose: Hard unsatisfiable instance for constant-depth multilinear IPS over finite fields
Explicitly constructed; its hardness is the paper's main theorem, so it is not an independent falsifiable entity.
ks_{w,e2} (symmetric knapsack of degree 2)
purpose: Separation instance between finite fields and characteristic 0
Explicit construction used to show that constant-depth multilinear IPS differs across characteristics.
f = prod(1-x_i) - 2 and its lifted version f^*(z,x)
purpose: Hard instances for roABP-IPS over finite fields
Explicit polynomials used in the functional-method roABP lower bounds.
unsatisfiable system (f,g,x^2-x) with f=prod_{i<j}(x_i+x_j+1), g=prod(1-x_i)-1
purpose: Hard instance for the multiples-method roABP-IPS lower bound
Explicit system; the choice of g avoids the large-characteristic dependence of the earlier FSTW21 instance.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Lower Bounds against the Ideal Proof System in Finite Fields." pith.science (2026). https://pith.science/paper/HFD3TTJK

@misc{pith2026250617210,
  author       = {Pith},
  title        = {Pith review of: Lower Bounds against the Ideal Proof System in Finite Fields},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HFD3TTJK}},
  note         = {Machine review of arXiv:2506.17210}
}

abstract

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. All of these bounds, however, are proved only over large (or characteristic $0$) fields, yet finite fields are the more natural setting for propositional proof complexity, especially for progress toward lower bounds for Frege systems such as $AC^0[p]$-Frege. This work establishes lower bounds against fragments of IPS over fixed finite fields. Specifically, we show that a variant of the knapsack instance studied by Govindasamy, Hakoniemi, and Tzameret (FOCS'22) has no polynomial-size IPS refutation over finite fields when the refutation is multilinear and written as a constant-depth circuit. The key ingredient of our argument is the recent set-multilinearization result of Forbes (CCC'24), which extends the earlier result of Limaye, Srinivasan, and Tavenas (FOCS'21) to all fields, and an extension of the techniques of Govindasamy, Hakoniemi, and Tzameret to finite fields. We also separate this proof system from the one studied by Govindasamy, Hakoniemi, and Tzameret. In addition, we present new lower bounds for read-once algebraic branching program refutations, roABP-IPS, in finite fields, extending results of Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.'21) and Hakoniemi, Limaye, and Tzameret (STOC'24). Finally, we show that any lower bound against any proof system at least as strong as (non-multilinear) constant-depth IPS over finite fields for any instance, even a purely algebraic instance (i.e., not a translation of a Boolean formula or CNF), implies a hard CNF formula for the respective IPS fragment, and hence an $AC^0[p]$-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J. ACM'18)).

Figures

Figures reproduced from arXiv: 2506.17210 by the authors.

**Figure 1.** From [GHT22]. Illustration of a word w. Each index wi of w is shown as a box with wi slots, so every variable x (i) σ in X(wi) appears as the string σ written inside its corresponding box. The word w shown is balanced. the positive and negative variables in the definition below. We define the positive overlap of w, denoted ∆G(Pw), as the maximum degree of a vertex in Pw. Similarly, the negative overlap, denoted ∆G(N… view at source ↗

**Figure 2.** From [GHT22]. Here ∗ represents either 0 or 1. In the construction of the polynomial ksw,p, for i = 2 and σ = 011001, we see that f (2) 011001 = y (1) 011 · y (3) 00 · (1 − (1 − y (4) 1000)(1 − y (4) 1001)· · ·(1 − y (4) 1111)). While our construction of f (i) σ differs from [GHT22], it still functions as an indicator for the variable x (i) σ . Comment (computing ksw,p by a poly(d, 2 bp)-size, product-depth 3, multi… view at source ↗

**Figure 3.** From [GHT22]. In this example, T = {1, 4, 7, 8} ⊆ Nw and m = y (1) 100 · y (4) 1001 · y (7) 0110 · y (8) 11 is a set-multilinear monomial over w|T . Like [GHT22], since S = {5, 6} is the maximal subset of Pw with AS w ⊆ BT w , we have that the leading monomial of gm(x) is less than or equal to x (5) 00 · x (6) 101101. However, in contrast to [GHT22], in our polynomial ksw,p, the partial assignment setting the y-vari… view at source ↗

Figures from the paper (1 more)

**Figure 4.** Figure 4: Illustration of the scattered partition induced by π : Pw → [∆G(Nw)] with ∆G(Nw) = 3. The values of π appear above the positive boxes, while the neighbourhoods of the positive indices are shown below the negative boxes. Since this is a scattered partition, vertices in …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

17 extracted references · 7 canonical work pages

[4]

Theorie des Fonctions Numeriques Simplement Periodiques

Full Version:http : //arxiv.org/abs/1412.8746. 2018, pp. 1424–1462. [Luc78] Edouard Lucas. “Theorie des Fonctions Numeriques Simplement Periodiques”. In:Amer. J. Math.1.2 (1878), pp. 184–196.issn: 0002-9327.doi:10.2307/2369308.url:https://doi. org/10.2307/2369308. [Nis91] Noam Nisan. “Lower Bounds for Non-Commutative Computation”. In:STOC

arXiv 2018
[10]

Lower Bounds for Polynomial Cal- culus with Extension Variables over Finite Fields

Ed. by Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller. ACM, 2020, pp. 591–603.doi:10.1145/3373718. 3394754.url:https://doi.org/10.1145/3373718.3394754. [IMP23] Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. “Lower Bounds for Polynomial Cal- culus with Extension Variables over Finite Fields”. In: CCC ’23. Warwick, United Kingdom: S...

arXiv 2020
[11]

Characterizing Propositional Proofs as Non- commutative Formulas

IEEE, 2021, pp. 804– 814.doi:10.1109/FOCS52979.2021.00083.url:https://doi.org/10.1109/FOCS52979. 2021.00083. [LTW18] Fu Li, Iddo Tzameret, and Zhengyu Wang. “Characterizing Propositional Proofs as Non- commutative Formulas”. In:SIAM Journal on Computing. Vol

arXiv 2021
[17]

Iterated Lower Bound Formulas: A Diagonalization- Based Approach to Proof Complexity

Chicago, IL, USA: Association for Computing Machinery, 2020, pp. 78–90.isbn: 9781450369794.doi:10.1145/ 3357713.3384288.url:https://doi.org/10.1145/3357713.3384288. [ST25] Rahul Santhanam and Iddo Tzameret. “Iterated Lower Bound Formulas: A Diagonalization- Based Approach to Proof Complexity”. In:SIAM Journal on Computing0.0 (2025), STOC21- 313-STOC21–349...

arXiv 2025
[31]

Unsolvable systems of equations and proof complexity

DIMACS Ser. Discrete Math. Theoret. Comput. Sci. Providence, RI: Amer. Math. Soc., 1997, pp. 215–244. [Pit98] Toniann Pitassi. “Unsolvable systems of equations and proof complexity”. In:Proceedings of the International Congress of Mathematicians, Vol. III (Berlin, 1998). Vol. III. 1998, pp. 451–

work page 1997
[200]

Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits

LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2021, 21:1–21:18.doi:10.4230/LIPIcs.CCC.2021.21.url: https://doi.org/10.4230/LIPIcs.CCC.2021.21. [BDS24] C.S. Bhargav, Sagnik Dutta, and Nitin Saxena. “Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits”. In:ACM Trans. Comput. Theory16.4 (Nov. 2024). issn: 1942-3454.d...

work page doi:10.4230/lipics.ccc.2021.21.url: 1996
[261]

A Lower Bound for Polynomial Calculus with Extension Rule

Leibniz International Proceedings in In- formatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, 2023, 12:1–12:20.isbn: 978-3-95977-278-5.doi:10 . 4230 / LIPIcs . ICALP . 2023 . 12.url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.12. [Ale21] Yaroslav Alekseev. “A Lower Bound for Polynomial Calc...

work page doi:10.4230/lipics.icalp.2023.12 2023
[300]

Quasipolynomial-Time Identity Testing of Non- commutative and Read-Once Oblivious Algebraic Branching Programs

LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2024, Art. No. 31, 16.doi:10.4230/lipics.ccc.2024.31. url:https://doi.org/10.4230/lipics.ccc.2024.31. [FS13] Michael A. Forbes and Amir Shpilka. “Quasipolynomial-Time Identity Testing of Non- commutative and Read-Once Oblivious Algebraic Branching Programs”. In:FOCS

doi:10.4230/lipics.ccc.2024.31 2024

Show all 17 references

[305]

Low-depth algebraic circuit lower bounds over any field

LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2024, Art. No. 10, 20.doi:10.4230/lipics.sat. 2024.10.url:https://doi.org/10.4230/lipics.sat.2024.10. [For24] Michael A. Forbes. “Low-depth algebraic circuit lower bounds over any field”. In:39...

2024 doi
[460]

Algebraic Proof Complexity: Progress, Frontiers and Challenges

[PT16] Tonnian Pitassi and Iddo Tzameret. “Algebraic Proof Complexity: Progress, Frontiers and Challenges”. In:ACM SIGLOG News3.3 (2016). Ed. by Andrzej Murawski. 38 [RT08a] Ran Raz and Iddo Tzameret. “Resolution over linear equations and multilinear proofs”. In: Ann. Pure App...

2016 doi
[1991]

Algebraic propositional proof systems

1991, pp. 410–418.doi:10.1145/103418.103462. [Pit97] Toniann Pitassi. “Algebraic propositional proof systems”. In:Descriptive complexity and finite models (Princeton, NJ, 1996). Vol

1991
[2012]

(Semi)Algebraic proofs over±1 variables

[Sap22] Ramprasad Saptharishi.A survey of lower bounds in arithmetic circuit complexity. 2016-2022. url:%5Curl%7Bhttps://github.com/dasarpmar/lowerbounds-survey/releases%7D. [Sok20] Dmitry Sokolov. “(Semi)Algebraic proofs over±1 variables”. In:Proceedings of the 52nd An- nual ...

2016
[2013]

Proof Complexity Lower Bounds from Algebraic Circuit Complexity

ArXiv 1209.2408. 2013, pp. 243–252.doi:10.1109/FOCS.2013.34. [FSTW21] Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. “Proof Complexity Lower Bounds from Algebraic Circuit Complexity”. In:Theory Comput.17 (2021), pp. 1–88. url:https://theoryofcomputing.org/a...

2021 arXiv
[2020]

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

ACM, 2020, pp. 54–67. [AGKST23] Prashanth Amireddy, Ankit Garg, Neeraj Kayal, Chandan Saha, and Bhargav Thankey. “Low- Depth Arithmetic Circuit Lower Bounds: Bypassing Set-Multilinearization”. In:50th Interna- tional Colloquium on Automata, Languages, and Programming (ICALP 20...

2020
[2022]

Semi-algebraic proofs, IPS lower bounds, and theτ-conjecture: can a natural number be negative?

arXiv:2112.00792.url:https://arxiv.org/ abs/2112.00792. 36 [AGHT20] Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. “Semi-algebraic proofs, IPS lower bounds, and theτ-conjecture: can a natural number be negative?” In:Pro- ceedings of the 52nd Annual ACM...

arXiv
[2024]

The Surprising Power of Constant Depth Algebraic Proofs

Vancouver, BC, Canada: Association for Computing Machinery, 2024, pp. 1396–1404.isbn: 9798400703836.doi:10.1145/3618260. 3649616.url:https://doi.org/10.1145/3618260.3649616. [IMP20] Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. “The Surprising Power of Constant Depth...

2024
[2025]

TowardsNP-Pvia Proof Complexity and Search

[Bus12] Samuel Buss. “TowardsNP-Pvia Proof Complexity and Search”. In:Annals of Pure and Applied Logic163.7 (2012), pp. 906–917. [CEI96] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. “Using the Groebner basis algo- rithm to find proofs of unsatisfiability”. In:Proce...

2012

Pith tools

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

[1] [4]

Theorie des Fonctions Numeriques Simplement Periodiques

Full Version:http : //arxiv.org/abs/1412.8746. 2018, pp. 1424–1462. [Luc78] Edouard Lucas. “Theorie des Fonctions Numeriques Simplement Periodiques”. In:Amer. J. Math.1.2 (1878), pp. 184–196.issn: 0002-9327.doi:10.2307/2369308.url:https://doi. org/10.2307/2369308. [Nis91] Noam Nisan. “Lower Bounds for Non-Commutative Computation”. In:STOC

arXiv 2018

[2] [10]

Lower Bounds for Polynomial Cal- culus with Extension Variables over Finite Fields

Ed. by Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller. ACM, 2020, pp. 591–603.doi:10.1145/3373718. 3394754.url:https://doi.org/10.1145/3373718.3394754. [IMP23] Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. “Lower Bounds for Polynomial Cal- culus with Extension Variables over Finite Fields”. In: CCC ’23. Warwick, United Kingdom: S...

arXiv 2020

[3] [11]

Characterizing Propositional Proofs as Non- commutative Formulas

IEEE, 2021, pp. 804– 814.doi:10.1109/FOCS52979.2021.00083.url:https://doi.org/10.1109/FOCS52979. 2021.00083. [LTW18] Fu Li, Iddo Tzameret, and Zhengyu Wang. “Characterizing Propositional Proofs as Non- commutative Formulas”. In:SIAM Journal on Computing. Vol

arXiv 2021

[4] [17]

Iterated Lower Bound Formulas: A Diagonalization- Based Approach to Proof Complexity

Chicago, IL, USA: Association for Computing Machinery, 2020, pp. 78–90.isbn: 9781450369794.doi:10.1145/ 3357713.3384288.url:https://doi.org/10.1145/3357713.3384288. [ST25] Rahul Santhanam and Iddo Tzameret. “Iterated Lower Bound Formulas: A Diagonalization- Based Approach to Proof Complexity”. In:SIAM Journal on Computing0.0 (2025), STOC21- 313-STOC21–349...

arXiv 2025

[5] [31]

Unsolvable systems of equations and proof complexity

DIMACS Ser. Discrete Math. Theoret. Comput. Sci. Providence, RI: Amer. Math. Soc., 1997, pp. 215–244. [Pit98] Toniann Pitassi. “Unsolvable systems of equations and proof complexity”. In:Proceedings of the International Congress of Mathematicians, Vol. III (Berlin, 1998). Vol. III. 1998, pp. 451–

work page 1997

[6] [200]

Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits

LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2021, 21:1–21:18.doi:10.4230/LIPIcs.CCC.2021.21.url: https://doi.org/10.4230/LIPIcs.CCC.2021.21. [BDS24] C.S. Bhargav, Sagnik Dutta, and Nitin Saxena. “Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits”. In:ACM Trans. Comput. Theory16.4 (Nov. 2024). issn: 1942-3454.d...

work page doi:10.4230/lipics.ccc.2021.21.url: 1996

[7] [261]

A Lower Bound for Polynomial Calculus with Extension Rule

Leibniz International Proceedings in In- formatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, 2023, 12:1–12:20.isbn: 978-3-95977-278-5.doi:10 . 4230 / LIPIcs . ICALP . 2023 . 12.url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.12. [Ale21] Yaroslav Alekseev. “A Lower Bound for Polynomial Calc...

work page doi:10.4230/lipics.icalp.2023.12 2023

[8] [300]

Quasipolynomial-Time Identity Testing of Non- commutative and Read-Once Oblivious Algebraic Branching Programs

LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2024, Art. No. 31, 16.doi:10.4230/lipics.ccc.2024.31. url:https://doi.org/10.4230/lipics.ccc.2024.31. [FS13] Michael A. Forbes and Amir Shpilka. “Quasipolynomial-Time Identity Testing of Non- commutative and Read-Once Oblivious Algebraic Branching Programs”. In:FOCS

doi:10.4230/lipics.ccc.2024.31 2024