Propositional proof complexity is an area of complexity theory that addresses the question of whether the class NP is closed under complement, and also provides a theoretical framework for studying practical applications such as SAT solving.
Some of the most well-studied contradictions are random $k$-CNF formulas where each clause of the formula is chosen uniformly at random from all possible clauses.
If the clause-to-variable ratio is chosen appropriately, then with high probability such a formula will be unsatisfiable, and the lack of structure in these formulas makes them natural candidates for proving lower bounds on the size of refutations in strong systems such as Frege systems where basically no nontrivial lower bounds are known.

In this work we prove exponential lower bounds on treelike resolution refutations of random 3-CNFs using new combinatorial techniques. The basic idea is to show that any formula with a short refutation can be compressed in a way that a random formula cannot be by algorithmically constructing such a short encoding.
It is important to emphasize that the actual results in the work are not new; exponential lower bounds for random $k$-CNFs are already known for treelike resolution, and in fact for much stronger systems such as general resolution and the RES$(k)$ system.
However, it is our hope that these new techniques generalize in a way that the known combinatorial techniques based on size-width tradeoffs do not, and that we can use these encoding techniques to attack stronger systems such as constant depth Frege systems where the old techniques are not applicable.