Cutting Planes is a proof system which certifies a system of linear inequalities has no integer solution by repeatedly deriving new inequalities by linear combinations and rounding-up of previous inequalities. As a proof system, it is strictly stronger than resolution - and lower bounds for it are hard to prove. The only known technique is the Monotone Interpolation Property, which in turn uses lower bounds from monotone circuit complexity. However, currently this technique can be used only for a very restrictive set of CNFs - it's not yet known if random constant-width CNFs are hard for Cutting Planes. We shall describe the MIP technique and mention some open problems on which there has been exciting progress in the past few years.
