A collapse result for constant depth propositional proof systems with modular counting connectives

A major open problem in propositional proof complexity is to obtain strong (ideally, exponential) lower bounds for the size of proofs of tautologies in constant depth proof systems with the usual boolean connectives and a parity connective (or, more generally, a mod p counting connective, where p is prime). I will say a few words about the problem itself and then try to explain a recent joint result with Sam Buss and Konrad Zdanowski: the depth of a constant depth proof involving the parity connective can be reduced to 3 at the cost of a quasipolynomial blowup in size.