A canonical communication problem ${\rm Search}(\phi)$ is defined for every unsatisfiable CNF $\phi$: an assignment to the variables of $\phi$ is distributed among the communicating parties, they are to find a clause of $\phi$ falsified by this assignment. Lower bounds on the randomized $k$-party communication complexity of ${\rm Search}(\phi)$ in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula $\phi$ in the semantic proof system ${\rm T}^{cc}(k,c)$ that operates with proof lines that can be computed by $k$-party randomized communication protocol using at most $c$ bits of communication [Göös, Pitassi, 2014]. All known lower bounds on ${\rm Search}(\phi)$ (e.g. [Beame, Pitassi, Segerlind, 2007; Göös, Pitassi, 2014; Impagliazzo, Pitassi, Urquhart, 1994]) are realized on ad-hoc formulas $\phi$ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas.

First, we demonstrate our approach for two-party communication and apply it to the proof system ${\rm Res}(\oplus)$ that operates with disjunctions of linear equalities over $\mathbb{F}_2$ [Itsykson, Sokolov, 2014]. Let a formula ${\rm PMP}_G$ encode that a graph $G$ has a perfect matching.
If $G$ has an odd number of vertices, then ${\rm PMP}_{G}$ has a tree-like ${\rm Res}(\oplus)$-refutation of a polynomial-size [Itsykson, Sokolov, 2014]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound $2^{\Omega(n)}$ on size of tree-like ${\rm Res}(\oplus)$-refutations of ${\rm PMP}_{K_{n+2,n}}$.

Then we apply our approach for $k$-party communication complexity in the NOF model and obtain a $\Omega\left(\frac{1}{k} 2^{n/2k - 3k/2}\right)$ lower bound on the randomized $k$-party communication complexity of ${\rm Search}({\rm BPHP}^{M}_{2^n})$ w.r.t. to some natural partition of the variables, where ${\rm BPHP}^{M}_{2^n}$ is the bit pigeonhole principle and $M=2^n+2^{n(1-1/k)}$.
In particular, our result implies that the bit pigeonhole requires exponential tree-like ${\rm Th}(k)$ proofs, where ${\rm Th}(k)$ is the semantic proof system operating with polynomial inequalities of degree at most $k$ and $k= O(\log^{1-\epsilon} n)$ for some $\epsilon > 0$.
We also show that ${\rm BPHP}^{2^n+1}_{2^n}$ superpolynomially separates tree-like ${\rm Th}(\log^{1-\epsilon} m)$ from tree-like ${\rm Th}(\log m)$, where $m$ is the number of variables in the refuted formula.