Monday, 10 August 2026
Lower bounds for monotone Boolean and real circuits.
Tree Resolution, lower bounds via Prover-Delayer games.
General Resolution, the size-width relation as a lower-bound technqiue.
Some query lower bounds.
Communication Complexity - the basic set up.
-
Tuesday, 11 August 2026
TBA
Brief overview of Frege and subclasses
TBA
-
Wednesday, 12 August 2026
TBA
Semi-algebraic systems SA
Brief overview of IPS
-
TBA
Thursday, 13 August 2026
TBA
TBA
TBA
TBA
Friday, 14 August 2026
TBA
TBA
-
TBA
Monday, 17 August 2026
Fix a set V of m vectors in F_2^n and define the following computational problem: given a subset S of V, is S full-rank? This problem is monotone (w.r.t. S) and easily solved in non-monotone NC2. We show that this problem has no monotone Boolean circuits of size exp(n^{1/3-o(1)}). This resolves a question of Jukna and Seiwert (2020) and yields the best known monotone vs. non-monotone separation for a function in NC.
Joint work with Bruno Cavalar (Oxford), Théo Borém Fabris (U. Copenhagen), Partha Mukhopadhyay (CMI) and Amir Yehudayoff (U. Copenhagen)
In this talk, we explore the torus polynomial approximation based approach towards a long-standing question: whether AND can be computed by CC^0 circuits - the class of constant-depth polynomial size circuits containing MOD_m gates for some natural number m.
In this talk, we describe lower bound arguments against symmetric CC^0-circuits for computing AND. More precisely, we prove that any depth h symmetric CC^0 circuit requires 2^{Omega(n^{1/O(h)})) size to compute AND. The technique we use - the torus polynomial approximation - was introduced by Bhrushundi, Hosseini, Lovett and Rao (ITCS 2019) as an approach for proving lower bounds against ACC0 - a class containing CC0 where the circuits are also allowed AND, OR and NOT gates. We will describe this framework as wel, in the talk.
Joint work with Vaibhav Krishan (IMSc)
The Ideal Proof System was introduced by Grochow and Pitassi [GP18] and its study is a central topic in algebraic proof complexity. It was developed in the context of Nullstellensatz refutation [BIKP94] and is known to simulate Extended
Frege efficiently.
In this talk we will see a nearly quadratic-size formula lower bound for any multilinear IPS refutation of a variant of the subset-sum axiom polynomial.
We will also an exponential-size sum-of-ROABPs lower bound for any IPS refutation of a variant of the subset-sum axiom polynomial.
The talk is based on joint work with Utsab Ghosal, Partha Mukhopadhyay and Amit Sinhababu.
Ideal Proof System is an algebraic proof system, where the complexity of proof is measured in terms of algebraic complexity of the polynomials involved. One of the methods of proving lower bounds against IPS is functional method, which "transfers" syntactic lower bounds to IPS lower bounds. In this talk, we will see how to use functional method for proving lower bounds against restricted classes of IPS over large fields of positive characteristic. This is based on a joint work with Nutan Limaye, Varun Ramanathan, and Srikanth Srinivasan (https://eccc.weizmann.ac.il/report/2025/079/).
We exhibit an n-bit partial function with randomized communication complexity O(log n) but such that any completion of this function into a total one requires randomized communication complexity n^Ω(1). In particular, this shows an exponential separation between randomized and pseudodeterministic communication protocols. Previously, Gavinsky (2025) showed an analogous separation in the weaker model of parity decision trees. We use lifting techniques to extend his proof idea to communication complexity.
This is a joint work with Mika Göös, Nathaniel Harms, Artur Riazanov, Dmitry Sokolov, Weiqiang Yuan
The log-rank conjecture is a longstanding open problem with multiple equivalent formulations in complexity theory and mathematics. In its linear-algebraic form, it asserts that the rank and partitioning number of a Boolean matrix are quasi-polynomially related.
In this talk, I will present a relaxed but still equivalent version of the conjecture based on a new matrix parameter, $\pm$-rank: the minimum number of all-1 rectangles needed to express the Boolean matrix as a $\pm 1$-sum. $\pm$-rank lies between rank and partition number, and our main result shows that it is in fact equivalent to rank up to a logarithmic factor. This reframes the log-rank conjecture as: can every signed decomposition of a Boolean matrix be made positive with only quasi-polynomial blowup?
Additionally, I will show that the log-rank conjecture is equivalent to a conjecture on cross-intersecting set systems.
The talk is based on joint work with Shachar Lovett and Morgan Shirley.
Tuesday, 18 August 2026
Consider the following algorithm for finding a falsified clause of an unsatisfiable CNF formula, given an assignment: sequentially check each clause to see if it is falsified. As the formula is unsatisfiable, the algorithm clearly finds a falsified clause. However, proving that this algorithm is correct (outputs a falsified clause on every unsatisfiable CNF formula) is tantamount to showing NP=coNP! In this talk we will look at provably correct algorithms which find falsified clauses for subsets of unsatisfiable formulas, and show that these are equivalent to certain strong proof systems. Doing so will allow us to prove that two strong, and seemingly different, proof systems G1 and implicit resolution are polynomially equivalent, and develop a theory of provable reductions in TFNP.
TFZPP is the class of total NP search problems which can be solved by polynomial time randomized algorithms. We prove that in the black-box setting, TFZPP can be separated from all major TFNP classes. We initiate work on developing a taxonomy of TFZPP problems.
Based on joint work with Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, and Weiqiang Yuan which appeared at ITCS 2026.
Unlike in TFNP, for which there is an abundance of problems capturing natural existence principles which are incomparable (in the black-box setting), Kleinberg et al. [KKMP21] observed that many of the natural problems considered so far in the second level of the total function polynomial hierarchy (TFΣ2) reduce to the Strong Avoid problem.
In this work, we prove that the Linear Ordering Principle does not reduce to Strong Avoid in the black-box setting, exhibiting the first TFΣ2 problem that lies outside of the class of problems reducible to Strong Avoid.
The proof of our separation exploits a connection between total search problems in the polynomial hierarchy and proof complexity, recently developed by Fleming, Imrek, and Marciot [FIM25]. In particular, this implies that to show our separation, it suffices to show that there is no small proof of the Linear Ordering Principle in a Σ2-variant of the Sherali-Adams proof system. To do so, we extend the classical pseudo-expectation method to the Σ2 setting, showing that the existence of a Σ2 pseudo-expectation precludes a Σ2 Sherali-Adams proof. The main technical challenge is in proving the existence of such a pseudo-expectation, we manage to do so by solving a combinatorial covering problem about permutations. We also show that the extended pseudo-expectation bound implies that the Linear Ordering Principle cannot be reduced to any problem admitting a low-degree Sherali-Adams refutation.
G\"{o}\"{o}s et al. showed that $\Res \wedge \uSA = \revres$ in the following sense: if a formula $\phi$ has refutations of size at most $s$ and width/degree at most $w$ in both $\Res$ and $\uSA$, then there is a refutation for $\phi$ of size at most $\poly(s \cdot 2^w)$ in $\revres$. Their proof relies on the TFNP characterization of the aforementioned proof systems.
In this talk, we dicuss a direct and simplified proof of this result, simultaneously achieving better bounds: we show that if for a formula $\phi$ there are refutations of size at most $s$ in both $\Res$ and $\uSA$, then there is a refutation of $\phi$ of size at most $\poly(s)$ in $\revres$. This potentially allows us to ``lift'' size lower bounds from $\revres$ to $\Res$ for the formulas for which there are upper bounds in $\uSA$. This kind of lifting was not possible before because of the exponential blow-up in size from the width.
Finally, we generalize those intersection theorems to some proof systems for which we currently do not have a TFNP characterization.
Resolution over parities (Res(+)) extends the resolution proof system to allow linear algebra mod 2. While no strong lower bounds are known for this proof system, Efremenko and Itsykson (2025) proved exponential lower bounds when the depth is restricted to O(N log N) where N is the number of variables of the CNF formula.
We prove exponential lower bounds against Res(+) refutations of almost quadratic depth. The lifted Tseitin formula we consider has O(N) clauses of width 6, which lets the allowed depth be almost quadratic not only in the number of variables, but also in the CNF size. We also prove depth-restricted lower bounds for variants of the bit pigeonhole principle, including an exponential lower bound for Res(+) proofs of the standard bit pigeonhole principle when the depth is almost quadratic.
Joint work with Sreejata Bhattacharya, Arkadev Chattopadhyay and Russell Impagliazzo
In this talk, we discuss the propositional proof system resolution over parities ($\text{Res}(\oplus)$), which extends standard resolution by operating with disjunctions of linear equations modulo 2. The main open problem for this system, proving a superpolynomial lower bound on the proof size, remains unresolved. Nevertheless, we contribute to the study of the bounded-depth case.
We show that for any unsatisfiable CNF formula $\varphi$ that requires resolution refutation width at least $w$, and for any $1$-stifling gadget $g$ (for example, $g=MAJ_3$), (1) every Res($\oplus$) refutation of the lifted formula $\varphi \circ g$ of size at most $S$ has depth at least $\Omega(w^2/\log S)$; (2) every $\resoplus$ refutation of the lifted formula $\varphi \circ g$ has size $\Omega(w^2)$.
Our proof combines the random-walk-with-restarts method of Alekseev and Itsykson [STOC 2025] with a new idea: the random walk is defined relative to the structure of the refutation graph, rather than by a distribution on inputs induced by the formula.
We establish two applications of our technique. First, we construct a family of polynomial-size formulas that admit polynomial-size resolution refutations, while any Res($\oplus$) refutation of depth $o(n^2/\log^4 n)$ requires superpolynomial size.
Second, we prove that, for every constant $\varepsilon$>0, automatability is NP-hard for any propositional proof system that lies between regular resolution and depth-$n^{2-\varepsilon}$ Res($\oplus$).
The talk is based on joint work with Vladimir Podolskii and Alexander Shekhovtsov.
Wednesday, 19 August 2026
"Consider a data structure problem with possible data coming from a set
$\mathcal D$, queries coming from a set $\mathcal Q$, and in the dynamic
case updates coming from a set $\mathcal U$. Then, the current state of
the art in data structure lower bounds is
$t = \tilde\Omega(\log |\mathcal Q|)$ for static data structure
problems, and
$\max(t_{\mathrm q},t_{\mathrm u}) = \tilde\Omega((\log n)^2)$ where
$n = \max(|\mathcal Q|,|\mathcal U|,\log |\mathcal D|)$ for dynamic.
We port Razborov and Rudich's natural-proofs framework to the setting of
static and dynamic data structures in the cell probe model, in a way
that strongly suggests this state of the art is unlikely to be improved
anytime soon. A similar direction was recently taken also by Korten,
Pitassi and Impagliazzo (FOCS 2025) who look at static data structure
lower bounds in a different regime of parameters. Our contribution is:
- We define notions analogous to pseudorandom functions (PRF). We call
these primitives *local PRFs*, in the context of static data
structures, and *local and locally updatable (LLU) PRFs*, in the
context of dynamic data structures.
- We then formulate cryptographic conjectures, namely, that secure
local PRFs and secure LLU PRFs exist, precisely at the frontier
where we are no longer able to prove static, respectively dynamic,
data structure lower bounds. If these conjectures are true, it
follows that the current state of the art in data structure lower
bounds cannot be improved by a natural proof.
- We show that (almost) every single known data structure lower bound
proof is a natural proof, by surveying all lower bounds in the
literature (known to us). (The only exception is proofs based on
lifting theorems.)
- It follows that, if our cryptographic conjecture is true, then all
known lower bound proof techniques (minus the two exceptions) are
unable to improve upon the state of the art. (We also present
obstacles for the two exceptions.)
- Further, we provide concrete candidate constructions for our two
pseudo-random primitives. We conjecture that our constructions are
secure for parameters just above the state-of-the-art lower bounds.
- We also show that, whether or not they are secure, our candidate
PRFs at least satisfy the natural properties appearing in all (but
one) known proofs.
- So if one is interested in improving upon the state of the art in
static or dynamic data structure lower bounds, one must either find
a non-natural method of proving such lower bounds (no such method
currently exists), or one may as well begin by trying to break our
PRF candidates."
Circuit complexity lower bounds for explicit functions are hard to prove. This has been true anecdotally but has also been backed up by the Natural Proof Barrier framework of Razborov and Rudich, which views lower bound proofs as computational tasks. It states that assuming the existence of a pseudorandom function generator supported on small circuits there is no "natural" lower bound proof that a function does not have a small circuit.
When restricting to constant depth circuits we are able to prove far stronger, subexponential, lower bounds. However improvements on these lower bounds have also been anecdotally hard to prove. We note that most state-of-the-art lower bound proofs for constant depth circuits are computational tasks that are computable by polysize constant depth circuits. More generally, we show that they are "AC0-natural". We then show that "AC0-natural" lower bound proofs cannot significantly improve the state of the art lower bounds. Notably we show this unconditionally by providing a construction of pseudorandom function generators supported on constant depth circuits of subexponential size that fool ALL polysize constant depth circuits. This is proven via the best known lower bounds against constant depth circuits, thereby using the lower bound itself to prove the hardness of improving the lower bound.
"We exhibit supercritical trade-off for monotone circuits, showing that
there are functions computable by small circuits for which any small
circuit must have depth superlinear or even super-polynomial in the number
of variables, far exceeding the linear worst-case upper bound. We obtain
similar trade-offs in proof complexity, where we establish the first
size-depth trade-offs for cutting planes and resolution that are truly
supercritical, i.e., in terms of formula size rather than number of
variables, and also show supercritical trade-offs between width and size
for treelike resolution.
Our results build on a new supercritical width-depth trade-off for
resolution, obtained by refining and strengthening the compression scheme
for the cop-robber game in [Grohe, Lichter, Neuen, and Schweitzer 2023].
This yields robust supercritical trade-offs for dimension versus iteration
number in the Weisfeiler–Leman algorithm, which also translate into
trade-offs between number of variables and quantifier depth in first-order
logic. Our other results follow from improved lifting theorems that might
be of independent interest.
This is joint work with Susanna F. de Rezende, Noah Fleming, Duri Andrea
Janett, and Shuo Pang presented at STOC '25."
We study the average-case hardness of establishing that a graph does not have a large clique in both proof and communication complexity. We show exponential lower bounds on the length of cutting planes and bounded-depth resolution over parities refutations of the binary encoding of clique formulas on randomly sampled dense graphs. Moreover, we show that the randomized communication complexity of finding a falsified clause in these formulas is polynomial.
Based on joint work with de Rezende, Engström, Ghannane, and Riazanov that appeared at ICALP'26.
We study the sparsity of real polynomial representations of Boolean functions in the De Morgan basis. We introduce a novel combinatorial characterization, called max-degree restriction trees, that provides local certificates of large sparsity. Using this characterization, we show that approximating a Boolean function, rather than computing it exactly, does not lead to substantially sparser representations—there is only a polynomial advantage on the logarithmic scale, up to polylog(n) factors. This is a sparsity analogue of the celebrated relation between exact and approximate degree established by Nisan and Szegedy (STOC, 1992). I will also discuss consequences of our results for the AND-query model and for the communication complexity of certain lifted functions.
This talk is based on joint work with Arkadev Chattopadhyay and Shachar Lovett.
A major open problem in quantum communication complexity is whether quantum protocols can be exponentially more efficient than classical protocols for computing total Boolean functions; the prevailing conjecture is that they cannot be so. In a seminal work, Razborov (2002) resolved this question for AND-functions of the form
$F(x,y)=f(x_1 \land y_1 , \cdots , ,x_n \land y_n)$,
when the outer function f is symmetric, by proving that their bounded-error quantum and classical communication complexities are polynomially related. Since then, extending this result to all AND-functions has remained open and has been posed by several authors.
In this work, we settle this problem in a strong way. We show that for every Boolean function f, the bounded-error quantum and classical deterministic communication complexities of the function $f \circ \text{AND}_2$ are polynomially related, up to polylogarithmic factors in n. We prove this by showing that both are characterized--up to polynomial loss--by the logarithm of the De Morgan sparsity of f.
Our results build on the recent work of Chattopadhyay, Dahiya, and Lovett (2025) on structural characterizations of non-sparse Boolean functions, which we extend to resolve the conjecture for general AND-functions
Thursday, 20 August 2026
The weak rank principle formalises the following algebraic fact: a matrix $A$ cannot be factorised as the product $XY$ when $X$ has fewer columns than the rank of $A$. We study the complexity of this principle in algebraic proof systems and show that it can be used as a proof complexity generator, with applications to the hardness of lower bound formulas.
The Lovász-Theta function of a graph is an important function which can be used to analyze several fundamental properties of a graph. In particular, the Lovász-Theta function is an upper bound on the Shannon capacity of a graph and the Lovász-Theta function of the complement of a graph is always between the clique number and the chromatic number of the graph.
For a random G(n,1/2) graph, it has long been known that the Lovász-Theta is a constant times the square root of n but the exact constant was unknown. In this work, we resolve this question by showing that with high probability, the Lovász-Theta function of a random graph is (1+o(1)) times the square root of n.
To prove this result, we give an intricate and novel construction of a candidate solution for the dual SDP for the Lovász-Theta function and show that with high probability, it is feasible and has value (1+o(1)) times the square root of n. In this talk, I will describe our construction and give intuition for why it works.
TBA
We study non-deterministic representation of Boolean functions by polynomials.
A polynomial $p(x)$ is said to be a \emph{non-deterministic polynomial} for a
Boolean function $f$ if for all $a\in \{0,1\}^n$, $p(a)\neq 0$ iff $f(a)=1$.
The \emph{non-deterministic degree} of $f$, denoted $\ndeg(f)$, is the
minimal degree of a non-deterministic polynomial for $f$.
In this talk, we will explore extremal properties of non-deterministic
represenation. In particular, we will show that almost all Boolean functions
on $n$ variables have non-deterministic degree at most
$n/2 + O(\sqrt{n\log n})$. This confirms a conjecture of (Iyer et al., 2023).
Furthermore, together with their lower bound, it establishes a tight bound on
the rational degree of random Boolean functions up to lower order terms.
We also disprove a conjecture of (Kothari et al., 2026) about effective
hypercube nullstellensatz for more than two polynomials.
This talk is based on a joint work with Sudharshan Rajagopalan (IIT Hyderabad).
Linearity testing is a fundamental property testing problem with many applications to several areas of TCS. It can be construed as testing for "polymorphisms" of the ternary Boolean predicate EvenParity. We prove an analogous statement for all predicates over the Boolean alphabet, and for some predicates over larger finite alphabets. Joint work with Yaroslav Alekseev appearing in FOCS 2026 (under the title "Approximate Polymorphisms").
An overview of recent developments in topological methods for use in separating pseudodeterministic and randomized communication complexity as well as tightly determining the sign rank of the gap-hamming problem.
Techniques involve Z2-equivariant topology and the design of replicable learning algorithms.
Friday, 21 August 2026
We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\varepsilon} \leq s(n) \leq 2^{n^{1-\varepsilon}}$ we exhibit an explicit family~$\calA$ of $n$-variate CNF formulas $A$, each of size~$|A| \le s(n)^{1+\eps}$, such that if~$A$ is chosen uniformly from~$\calA$, then \aas any tree-like Frege refutation of~$A$ in line-size~$s(n)$ is of length super-polynomial in~$|A|$. Our lower bounds apply also to tree-like degree-$d$ threshold systems, for $d \approx \log\bigl(s(n)\bigr)$, that is, for $d$ up to $n^{1-\eps}$. More generally, our lower bounds apply to the semantic version of these systems and to any semantic tree-like proof system where the number of distinct lines is bounded by $\exp\bigl(s(n)\bigr)$.
Joint work with Susanna de Rezende, David Engström, and Yassine Ghannane.
The red-blue pebble game is a well known two-player game on graphs that has been used in the past as a tool to analyze complexity measures in several computation models as well as proof systems. We define a new way to measure the cost of the game, the blue cost, which only counts the number of pebbles that are colored blue during the game. This new measure characterizes exactly several space bounds in tree-like and negative Resolution.
In particular we prove that for any unsatisfiable formula $F$, the clause space requirements of the formula in tree-like Resolution, exactly coincide with the minimum blue pebbling cost of the game played on a refutation graph of $F$ (not necessarily a tree). This exactly parallels the known result for general Resolution in terms of the standard black pebble game, and improves the existing approximated characterization of tree-like space in terms of reversible pebbling.
We show that the blue pebbling cost is also well suited for analyzing the space requirements of the lifted pebbling formulas $Peb_G[\vee]$ and $Peb_G[\oplus]$ in the two Resolution restrictions. In the case of tree-like Resolution, the clause space of $Peb_G[\vee]$ asymptotically coincides with the blue cost of the underlying graph $G$.
For the case of negative Resolution, we obtain almost matching upper and lower bounds for the space in the two classes of lifted formulas, similar to the ones existing for general Resolution.
We also prove a close to optimal space separation between tree-like and negative Resolution, presenting a class of formulas with $n$ variables that require clause space $\Omega(\frac{n}{\log n})$ in negative Resolution, but have constant space tree-like refutations. This contrasts with the fact that negative Resolution can simulate tree-like Resolution with a small increase in size.
"Quantified Boolean formulas (QBFs) extend propositional logic by allowing variables to be universally or existentially quantified, naturally capturing two-player games between an existential and a universal player. While the satisfiability of a QBF asks whether the existential player has a winning strategy, the corresponding counting problem (#QBF) asks how many such winning strategies exist. This problem is significantly more challenging than the analogous #SAT problem for propositional formulas.
This talk will present proof systems for #QBF, motivated by recent advances in the proof complexity of both QBF satisfiability and propositional model counting. It will begin with a simple baseline proof system for counting Skolem functions, and then examine systems based on the ∀-expansion rule of QBF proof systems. Both these approaches will be shown to have inherent structural limitations that give rise to lower bounds. To overcome these weaknesses, the talk will introduce Q-MICE, a new line-based proof system with sound inference rules for computing and certifying #QBF solutions, inspired by the MICE proof system for #SAT. Finally, the talk will highlight the strength of Q-MICE through several upper-bound results, including quantified versions of formulas that were previously known to be difficult for MICE. These results also separate Q-MICE from the naive #QBF proof systems. Beyond their theoretical significance, these proof systems provide a foundation for certifying and developing future #QBF solvers.
This work is in collaboration with Leroy Chew, Vaibhav Krishan and Anil Shukla. It has been accepted for publication in SAT 2026."
We present a generic way to obtain level lower bounds for (promise) CSP hierarchies from degree lower bounds for algebraic proof systems. More specifically, we show that pseudo-reduction operators in the sense of Alekhnovich and Razborov [Proc. Steklov Inst. Math. 2003] can be used to fool the cohomological k-consistency algorithm. As applications, we prove optimal level lower bounds for c vs. l-coloring for all l≥c≥3, and give a simplified proof of the lower bounds for lax and null-constraining CSPs of Chan and Ng [STOC 2025].
Real-world Boolean circuits are often fed input voltages that are unstable in addition to the stable values 0 and 1. The output of a circuit may be a valid stable value even when some of its inputs are unstable. For example, if the circuit is computing majority on 3 bits, two of its inputs are 1, and the third is unstable, then it may (and should) output 1. In this talk, we examine the circuit and formula complexity of functions when we demand that the circuit should output a stable value when it makes sense for it to do so.
In algebraic complexity theory, one typically studies algebraic models to compute polynomials over fields. As a generalization, one can consider polynomials over semirings; in particular, we’ll focus on min-plus semirings. Polynomials over min-plus semirings are min-of-sums and so, these correspond to several minimization problems (e.g., Travelling Salesman problem). Many dynamic programming algorithms (e.g., Bellman-Held-Karp algorithm for TSP) can be viewed as circuits over min-plus semirings. In this talk, we’ll discuss about algebraic branching programs (which are weaker than circuits) over min-plus semirings. In particular, we’ll talk about ABPs of small width (which are well-studied over fields) over min-plus semirings; here, restricting the width means that only a few DP table entries are allowed to be updated in each round/phase of the algorithm. Finally, we’ll discuss an analogue of the class VNP (which, over fields, is defined as hypercube sums over small circuits) over min-plus semirings, its relationship with VP, and its equivalent definitions in terms of weaker (than circuits) models. This talk will be based on joint discussions with Balagopal Komarath and Jayalal Sarma