63 citations · 77 across the 15 of their papers we have counts for
22 papers
The Weak Rank Principle: Lower Bounds and Applications
Michal Garl\'\ik, Svyatoslav Gryaznov, Hanlin Ren +1
Given two symbolic matrices and of dimensions and , the *weak rank principle* (WRank) states the equation is unsatisfiable when and ra…
Hard CNF Instances for Ideal Proof Systems
Tuomas Hakoniemi, Nutan Limaye, Iddo Tzameret
Since the introduction of the Ideal Proof System (IPS) by Grochow and Pitassi (J. ACM 2018), a substantial body of work has established size lower bounds for IPS and its fragments.…
AC^0[p]-Frege Cannot Efficiently Prove that Constant-Depth Algebraic Circuit Lower Bounds are Hard
Jiaqi Lu, Rahul Santhanam, Iddo Tzameret
We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas, J. ACM 2025; Forbes, CCC 2024) are ha…
Lower Bounds against the Ideal Proof System in Finite Fields
Tal Elbaz, Nashlen Govindasamy, Jiaqi Lu +1
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,…
Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers
Tuomas Hakoniemi, Nutan Limaye, Iddo Tzameret
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 propos…
Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
Albert Atserias, Iddo Tzameret
The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finit…
Stretching Demi-Bits and Nondeterministic-Secure Pseudorandomness
Iddo Tzameret, Lu-Ming Zhang
We develop the theory of cryptographic nondeterministic-secure pseudorandomness beyond the point reached by Rudich's original work (Rudich 1997), and apply it to draw new consequen…
Simple Hard Instances for Low-Depth Algebraic Proofs
Nashlen Govindasamy, Tuomas Hakoniemi, Iddo Tzameret
We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically,…
First-Order Reasoning and Efficient Semi-Algebraic Proofs
Fedor Part, Neil Thapen, Iddo Tzameret
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebra…
Semi-Algebraic Proofs, IPS Lower Bounds and the -Conjecture: Can a Natural Number be Negative?
Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch +1
We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems…
Uniform, Integral and Feasible Proofs for the Determinant Identities
Iddo Tzameret, Stephen A. Cook
Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for…
Resolution with Counting: Dag-Like Lower Bounds and Different Moduli
Fedor Part, Iddo Tzameret
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), thi…
Algebraic Proof Complexity: Progress, Frontiers and Challenges
Tonnian Pitassi, Iddo Tzameret
We survey recent progress in the proof complexity of strong proof systems and its connection to algebraic circuit complexity, showing how the synergy between the two gives rise to…
Proof Complexity Lower Bounds from Algebraic Circuit Complexity
Michael A. Forbes, Amir Shpilka, Iddo Tzameret +1
We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits c…
Characterizing Propositional Proofs as Non-Commutative Formulas
Fu Li, Iddo Tzameret, Zhengyu Wang
Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional calculus (i.e. Frege) proof is a proof starting from a set of axioms and deriving new…
Generating Matrix Identities and Proof Complexity
Fu Li, Iddo Tzameret
Motivated by the fundamental lower bounds questions in proof complexity, we initiate the study of matrix identities as hard instances for strong proof systems. A matrix identity of…
Sparser Random 3SAT Refutation Algorithms and the Interpolation Problem
Iddo Tzameret
We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of s…
Short Proofs for the Determinant Identities
Pavel Hrubes, Iddo Tzameret
We study arithmetic proof systems P_c(F) and P_f(F) operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field F. We es…
Short Propositional Refutations for Dense Random 3CNF Formulas
Sebastian Müller, Iddo Tzameret
Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many p…
Algebraic Proofs over Noncommutative Formulas
Iddo Tzameret
We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least…
Resolution over Linear Equations and Multilinear Proofs
Ran Raz, Iddo Tzameret
We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead…
Complexity of Propositional Proofs under a Promise
Nachum Dershowitz, Iddo Tzameret
We study -- within the framework of propositional proof complexity -- the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has…