Abstract
How hard is it to prove that a random k-CNF formula is unsatisfiable? Or to certify the chromatic number or the size of a maximum clique in a random graph? Many of the results demonstrating hardness of these problems for restricted computational models are obtained by proving a lower bound for the underlying method of reasoning, that is, for a particular proof system.
In this talk, we will survey some of the known average-case hardness results in proof complexity. In particular, we will consider what is known for the three mentioned problems—random k-CNF, k-coloring and k-clique—for the proof systems: resolution, polynomial calculus, sum-of-squares and cutting planes. We will also briefly touch upon some of the combinatorial structure present in random objects that are used to prove the known hardness results. No prior knowledge of proof complexity is assumed.