Tradeoffs for small-depth Frege proofs

We study the complexity of small-depth Frege proofs and give the first tradeoffs between the size of each line and the number of lines. Existing lower bounds apply to the overall proof size-the sum of sizes of all lines-and do not distinguish between these notions of complexity. For depth-d Frege proofs of the Tseitin principle where each line is a size-s formula, we prove that $\exp(n/2^{\Omega(d\sqrt{\log s})})$ many lines are necessary. This yields new lower bounds on line complexity that are not implied by $\mathbf{H}\mathop{\mathbf{a}}\!\!\!\!^{\circ}\mathbf{stad}$'s recent $\exp(n^{\Omega(1/d)})$ lower bound on the overall proof size. For $s$= poly $(n)$, for example, our lower bound remains $\exp(n^{1-o(1)})$ for all $d=o(\sqrt{\log n})$, whereas $\mathbf{H}\mathop{\mathbf{a}}\!\!\!\!^{\circ}\mathbf{stad}$'s lower bound is $\exp(n^{o(1)})$ once $d\ = \omega_{n}(1)$. Our main conceptual contribution is the simple obser-vation that techniques for establishing correlation bounds in circuit complexity can be leveraged to establish such tradeoffs in proof complexity.