Bounded Depth Frege Lower Bounds for Random 3-CNFs via Deterministic Restrictions

A major open problem in proof complexity is to show that random 3-CNFs with linear number of clauses require super-polynomial size refutations in bounded depth Frege. We make a first step towards this question by showing a super-linear lower bound: for every k, there exists ε > 0 such that any depth-k Frege refutation of a random n-variable 3-CNF with Θ(n) clauses has Ω(n1 + ε) steps w.h.p. Our proof involves a novel adaptation of the deterministic restriction technique of Chaudhuri and Radhakrishnan (STOC'96).