So, this is joint work with my advisor Russell and Tourniquet. So, an important open problem in proof complexity right now is lower bounds for AC0P freighter,

which is the proof system that works over constant depth circuits with modular counting aids. And, so in the circuit world, we have lower bounds for AC0P circuits through Rasparov and Smolensky and so they use algebraic methods for their lower bounds and so that pointed towards algebraic proof systems.

And, so one of the first algebraic proof systems, Nullstellensatz, so was actually introduced to show that it can give lower bounds for AC0 freighter with counting axioms, which is weaker notion than counting aids.

And, polynomial calculus was introduced as a generalization of Nullstellensatz. So, here is just a quick overview. So, a tautology is represented as a system of polynomials P1 to Pm over a field. And, essentially the system lets you work in the degree d pseudo-ideal, which means that given two polynomials, you can derive their linear combination

or you can multiply by a variable as long as you don't exceed degree d. And, the goal is to derive a contradiction. And, the size of the proof is measured in terms of the total number of monomials. And, we have strong degree and size lower bounds for Rasparov for PHP and CITIN.

And, so here is a quick overview of semi-algebraic proof systems. So, these lines in these thresholds, they are not believed to be in AC0P freighter because again in the circuit world, we don't have that majority in AC0P.

So, here is a quick intro. So, in cutting planes, we have a system of linear inequalities. And, we want to derive a contradiction using the linear combination or multiplying by a constant or dividing by a constant and rounding up.

And, in positive Stellensatz calculus, which is a generalization of sum of squares, it's a dynamic system. So, you are given a set of non-negative polynomials. And, you again want to derive a contradiction using linear combination or multiplication of non-negative polynomials or just introducing a square

and accepting that it should be positive. And, so now back to the question of AC0P freighter bounds. So, right now the state is that we have strong bounds for null Stellensatz and polynomial calculus. But, they have not been pushed to bounds for AC0P freighter.

And, so the natural next step would be to say, okay, let's try to strengthen these systems, give them more power and maybe lower bounds for those will give us more insight. So, the main message of our work here is that this approach may not work because some very intuitive ways of generalizing these systems

are much more powerful than AC0P freighter or they do things which we don't believe to be AC0P freighter. So, what is the natural way to generalize polynomial calculus? So, there have been many different generalizations proposed.

But, many of them are not Cook-Racow systems, which means that it's not known whether the proofs in the systems are verifiable and deterministic polynomial time. So, they usually require the use of polynomial identity testing. And, so here we focus on generalization by Grigoriev and Hirsch, which is Cook-Racow.

And, so the idea here is to introduce extension variables, which are functions of the original variables xi. So, I'm going to use xi's for the original variables and yz and so on for the extension variables. So, for instance, you can introduce extension variable y, which is a linear combination of the original variables.

And, so you can introduce a second extension variable, which is a product of these yi's and so on. So, this is just working with circuits? It's equivalent to working or working with circuits?

Yeah, like a straight line program. Yeah, I mean this recursive definition is very reminiscent of a straight line. So, the system depth dpc, we define it as allowing extension variables, which have up to d minus two alternating layers of this sum and product.

So, any proof line would be a depth d arithmetic circuit in the original variables. So, say these variables are d minus two each. So, the whole line would be a depth d arithmetic circuit in the original variables. And, the size here we measure in terms of the number of monomials in all of these variables,

which is again how you would measure size of straight line programs, for instance. So, what is known so far about depth dpc? So, we know that depth dpc is quite powerful.

So, here is a bit of notation. So, I use a arrow b for proof systems a and b to denote that b effectively simulates a. And, I'll clarify what is effective simulation in a bit. So, when Rigoriya and Hirsch introduced this system, they showed that depth dpc over fp simulates depth order d ac0p figure.

So, here the key thing is that these two depths have to scale together proportionally. And, they also showed that PHP and CITIN are easy for depth 3 PC over appropriate fields.

So, PHP would be over say rationals and CITIN would be over a field which contains the right root of unity. So, Raj and Samarit showed that cutting planes with bounded coefficients can be simulated by depth 3 PC over the rationals.

So, we show that depth 3 PC is in fact much more powerful.

So, we show that in fact depth 43 PC can simulate cutting planes and some of this.

So, the upper bound on the constant is 43. And, this is over any extension field which is larger than the bit complexity of the proof lines.

And, by bit complexity I mean the number of monomials times the bit length of the largest coefficient. So, it's just how you would naturally represent a proof line. And, so here I again want to make a comparison to Ido's talk in the morning.

So, here we start with the same idea as them is that if you want to do semi-algebraic reasoning over algebraic systems, you want to move from the polynomial to its bit representation.

So, in particular you want to say that its sine bit is zero for instance. That would say that the polynomial is positive or non-negative. But, there are a couple of key differences. So, the first difference is that they consider simulation in IPS because IPS is a really strong system.

So, they are concerned with going from this representation to the bit representation within the system. So, they are concerned with deriving the bit representation of the polynomial from the polynomial inside the system. And, so essentially they show that the binary value principle is both necessary

and sufficient for making the switch from the polynomial to its bit representation. Whereas, since we work in much weaker systems, we don't want the burden of switching these representations within our system.

So, here we assume that this switch is made offline which means this system is already given the bit representation of the polynomial to begin with. And, that is what it has to refute. And, this is essentially the idea of effective simulation where you say if you want to refute a tautology in a system.

So, before representing that tautology in the new system, you are allowed to pre-process it a bit and represent it so that the new representation is morally equivalent to the original one. And, the other key difference is so once you obtain the bit representation either online or offline.

So, now you have to actually use it to prove stuff inside the system. And, here again since they have a really powerful system which contains Frege and extended Frege. So, doing bit arithmetic in IPS is less of an issue here.

But, for us since we work in this weak system, it's really the most non-trivial part of our work comes from showing that you can do bit arithmetic in constant depth.

So, these are the two key differences. And, so for this theorem there is an alternate proof known in the literature for the case of cutting planes. So, it's known that cutting planes simulates a propositional threshold calculus of bust and clod.

So, this proof is due to Frege and since for our next theorem so we essentially simulate the rules of PTK in say depth 9 PC. So, combining these two results we have that cutting planes is in depth 3 PC.

But, the problem with this proof is that it's non-explicit and from this proof you cannot get the value of the simulation like the 43 that you saw earlier. And, so this is the only source I can find.

So, I just want to highlight that. So, they ask for a more direct proof and which is able to determine the value of depth. So, this is from the textbook Boolean functions and computational models. And, so our simulation is more explicit and gives this bound of code.

What is the cryo-check result? So, actually the cryo-check result is just this. So, the cutting planes is in this system PTK. So, this is with our algorithm.

And, this is apparently like a sketch of the proof. So, I'll try to sketch the proof of our results. So, first I'll just give an overview of how we simulate cutting planes and bounded coefficients in depth 3 PC.

This is the result of Raaz and Samrat. So, say you have a line which has small coefficients. So, in depth 3 PC you want to introduce a linear form which is the same as the one being thresholded here.

And, then we introduce another equation in terms of this y which essentially says that y only has to take the values which make this threshold true. So, this is just a big OR saying that y is only taking the values that satisfying this threshold. So, let's denote this constraint by y belongs to C where C is this range of values.

So, really the key idea for the simulation is that given two constraints in this form y in C1 and y in C2.

You can derive in depth 3 PC this line which says y is in the intersection of both of the sets. And, this happens to be sufficient to simulate cutting planes with bounded coefficients. I won't go into the details here.

So, now let me try to sketch the proof for the unbounded coefficient case. So, again in the circuit world it's well known that if you have a highway threshold gate it can be computed by a small depth majority circuits. So, a tight simulation was shown by Goldman-Hastel and Rasborough for this.

So, but the problem is for any such construction that we want to use we really need to prove the correctness of the construction in depth 3 PC. I'll say more about this in a bit but essentially what it means is that so given the construction we need to be

able to take it apart and kind of play around with it in order to be able to use it to prove stuff. So, and the issue with these constructions is they usually use stuff like

Chinese reminder which is really hard to reason with in these bounded depth systems. So, we use this other much simpler but maybe less optimal construction by Maciel and Thain. So, what is this construction? So, let's say we want to compute the threshold of n numbers a1 to an.

So, first we just try to compute the sum of these numbers in low depth. So, let's say each number is represented in binary and we choose a block length of about log n and we split the bits of each number into blocks of size log n.

And now for each number we think of it as being made up of two parts the odd part and the even part. And so in the odd part you have that you only pick the odd blocks and zero out the even blocks. And in the even part you only pick the even blocks and zero out the odd blocks.

So, now it's clearly the sum of a number is equal to the sum of its odd and even parts. And so the sum of all the numbers is just the sum of all the odd parts plus the sum of all the even parts. So, let's look at how to compute the sum of all the odd parts in low depth.

So, let's say we are summing up all of these blocks. So, each block is of log n bits and there are n blocks. So, the sum is at most n squared or two log n bits in length and so that's exactly two blocks.

So, when we sum up all these blocks so we never get the carry to the next stage. So, we always end up with exactly the right number of bits and then so then we can move forward and compute the sum of the next stage and so on. And because there is no carry so each bit in this sum can be represented in a brute force way in terms of these.

So, for instance maybe so the last bit would just be one or it would be zero if the sum of all these numbers is even. So, you can just write it out brute force because these numbers are really small. And similarly we can do the same with the even parts, summing up all the even parts.

And now we have this even sum and the odd sum. And so for the final step we just use one step of carry save addition to compute the sum of the even and odd parts. And since so carry save addition for just two numbers is low depth so we are okay.

And now so if you want to say now express a threshold you can just represent all these numbers in say two's complement representation and carry out the sum. And say for the sign bit of this just say that it is equal to zero.

So, that would just say that okay the threshold of this so the sum of these things is greater than or equal to zero. So, again as I said it's not sufficient to it's not sufficient that we just have this construction.

We also need to be able to use it in the system. And so actually really the most important property we use repeatedly in the simulation is to this.

So, here this S represents the sum obtained using this construction. So, this is essentially saying that if you sum n numbers using this construction it is the same as summing the first n minus one numbers using the construction. And for the last one just using your usual definition of addition. So, this is essentially saying that if you can prove this in depth CPC.

So, that's essentially saying that at any point you can interchange this construction with the usual addition. And I think that's intuitively proving the correctness of this construction in our system. So, because it's saying that you can always swap with the usual addition whenever you want.

So, this is one of the key things we needed to show. And we also needed to derive some other basic properties within the system. Some things like to represent multiplication we just use this construction and do shifted addition.

And we have to again prove that okay this is actually equivalent to multiplication. And again some arithmetic into complement with the sign bits and so in negating stuff and things like that.

So, for our other results we improve upon Grigoryev and Hurst result in two ways. So, first we show that depth nine PC would contain AC0Q for any depth.

But it would simulated quasi polynomial and the constant would go into the quasi polynomial here. And more importantly this works for any prime Q over this fixed extension FP. So, once again this is kind of going in the opposite direction of what happens in the circuit world.

So, in the circuit world the exact lower bound is that AC0Q cannot be like a mod Q cannot be computed over FP. So, and here we have this counter intuitive result that for any prime Q over a fixed extension FP you can do this simulation.

So, again there is a proof of alternate proof of a part of this result in the literature.

So, depth three AC0Q is known to be collapsed into depth three AC0Q with a quasi polynomial grow up. This is due to bus et al. And again so once we have this result if you use the result of Grigoryev and Hurst which would scale the depths proportionally.

So, maybe this it would put the depth three AC0F in some depth 10 PC. So, combining those two you could get the result for the case of Q equals P. But again as I mentioned our result is more general in the fact that it works for any Q.

And maybe it's a simpler alternate proof for the case of Q equals P. So, I just briefly sketched the proof of this result. So, again in the circuit world so Allender showed that so any AC0Q circuit can be converted to a quasi polynomial size what I call flat circuit.

So, circuit which looks like this which has a threshold gate at the top and mod Q gates in the middle and gates at the bottom. And so Maciel and Pitasi extended this to the proof complexity world.

And they said so if you have an AC0Q for the proof you know we know that you can convert each line into a circuit of this type. But they also build a proof system which is essentially a sequence calculus over these kind of circuits. And then they show that you can actually complete the proof fill in the gaps and get a proof in that new proof system from any AC0Q.

And so essentially what we do is we show that we can simulate this proof system of Maciel and Pitasi rule by rule.

And so again the key thing is again the CP star simulation that I mentioned earlier. So, we just use that to simulate the threshold and parity Q gates and we also need that to simulate like the cut rule in sequence.

And these are just some more of our results. So, if you allow the depth to scale proportionally we can show that that

TPC can actually simulate TC0 of Frege where the depth is allowed to go proportionally. And finally for the case of depth 3 we extend the result of Raas and Samaret to say that it can simulate semantic cutting planes with bounded coefficients over the rational numbers.

And so here are some open problems. So, one initial open problem that we considered was to prove lower bounds for PC over the plus minus some basis but this has already been answered.

So, we should talk to Dimitri if you want to know more. And so the other problem is prove lower bounds for depth 3 PC. So, this definitely contains a resilient but it could be also more powerful. And it would also be interesting to prove for a very restricted version of this depth 3 PC.

So, this is the system where your extension variables are only linear transformations. And it's interesting even to prove for this restriction version which doesn't really contain, it's not known that it contains polynomial calculus in them. So, but the CP star simulation still works for this case.

And lastly so our results need a large enough extension field. So, can we do the same over the base field or show that it's not possible.