An active line of research in proof complexity over the last decade has been the study of proof space and trade-offs between size and space. Such questions were originally motivated by practical SAT solving, but have also led to the development of new theoretical concepts in proof complexity of intrinsic interest and to results establishing nontrivial relations between space and other proof complexity measures. By now, the resolution proof system is fairly well understood in this regard, as witnessed by a sequence of papers leading up to [Ben-Sasson and Nordstrom 2008, 2011] and [Beame, Beck, and Impagliazzo 2012]. However, for other relevant proof systems in the context of SAT solving, such as polynomial calculus (PC) and cutting planes (CP), very little has been known.

We prove an $n^{\Omega(1)}/4^k$ lower bound on the randomized k-party communication complexity of depth 4 $\ensuremath {\sf AC}^0$ functions in the number-on-forehead (NOF) model for up to $\Theta(\log n)$ players. These are the first nontrivial lower bounds for general NOF multiparty communication complexity for any $\ensuremath {\sf AC}^0$ function for $\omega(\log\log n)$ players. For nonconstant k the bounds are larger than all previous lower bounds for any $\ensuremath {\sf AC}^0$ function even for simultaneous communication complexity. Our lower bounds imply the first superpolynomial lower bounds for the simulation of $\ensuremath {\sf AC}^0$ by $\ensuremath {\sf MAJ\circ SYM\circ AND}$ circuits, showing that the well-known quasi-polynomial simulations of $\ensuremath {\sf AC}^0$ by such circuits due to Allender (1989) and Yao (1990) are qualitatively optimal,-1pt even for formulas of small constant depth. We also exhibit a depth 5 formula in ${\ensuremath {\sf NP}^{cc}_k}-{\ensuremath {\sf BPP}^{cc}_k}$ for k up to $\Theta(\log n)$ and derive $\Omega(2^{\sqrt{\log n}/\sqrt{k}})$ lower bound on the randomized k-party NOF communication complexity of set disjointness for up to $\Theta(\log^{1/3} n)$ players, which is significantly larger than the $O(\log\log n)$ players allowed in the best previous lower bounds for multiparty set disjointness. We prove other strong results for depth 3 and 4 $\ensuremath {\sf AC}^0$ functions.

We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems -- tree resolution -- into formulas that require large rank in very strong proof systems, including any proof system that manipulates polynomials of degree at most k (known as Th(k) proofs). These include high degree versions of Lovasz-Schrijver and Cutting Planes proofs.