## Cutting Planes Proofs of Tseitin and Random Formulas

Noah Fleming

University of Toronto

May 5, 2020

Proof Complexity studies the length of proofs of propositional tautologies in various restricted proof systems. One of the most well-studied is the Cutting Planes proof system, which captures reasoning which can be expressed using linear inequalities. A series of papers proved lower bounds on the length of Cutting Planes using the method of feasible interpolation whereby proving lower bounds on the size of Cutting Planes lower bounds proofs of a certain restricted class of formulas is reduced to monotone circuit lower bounds.