General information

Proof complexity, naturally, studies proofs and its fundamental question, which is related to some of the most important questions in computer science, is the following:

Given a true statement A, how long is the shortest proof that A is true?

Proof complexity also analyzes methods for finding short proofs if they exist. Since, for example, the statement A could be "This code is bug-free" or "No solution to these constraints has value better than K", proof complexity has applications to many areas of computer science, including optimization and formal verification among others.

Proof complexity also gives us tools to analyze the power and limitations of entire classes of algorithms. For example:

As hinted at by these examples, part of proof complexity involves understanding the best methods for expressing and checking proofs which include methods other than logic, such as polynomial equations, or integer inequalities.

The past decade has seen major progress in proof complexity and new applications, with many open problems resolved and many more now ready for attack. This course will give an introduction to modern proof complexity that will cover the classics in the field, as well as many of the most exciting recent developments. Throughout, we will focus on the applications of proof complexity and its many open problems.



There is no single text that covers this material at the right level so we have detailed course notes. These cover somewhat more material than we will be able to go over in class. For some of the recent material involving sum-of-squares proofs, and semi-algebraic algebraic proofs more generally, we will use the recent monograph:

Survey talks:

Surveys of Proof Complexity