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:
- modern SAT solvers that are at the heart of much of the current work in formal methods in PL/SE can be understood in terms of resolution proofs.
- semi-definite programming based on sum-of-squares proofs is the best
algorithm we know for solving large classes of optimization problems.
In this case, the mere existence of a short proof that there is a solution is
already enough to guarantee that there is a good algorithm to find that solution.
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
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
Throughout, we will focus on the applications of proof complexity and its many
- Instructor: Paul Beame
- Time and Lectures link: Mondays and Wednesdays, beginning Sept 30, 2020 at 3:00-4:20 pm on Zoom.
- Work: short easy exercises to keep everyone following along, class participation, a final presentation from a selected list of papers/topics.
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
Surveys of Proof Complexity