Jakob Nordström / Teaching / Proof Complexity as a Computational Lens Winter 2025/26

Proof Complexity as a Computational Lens Winter 2025/26

Follow these shortcut links to go directly to the course news, short overview, schedule and course contents, lecturers, goals, requirements, course material, problem sets, and other proof complexity courses.

News

  • We have revised the schedule to have only two lectures per week going forward. This means that the scribing schedule will need to be revised slightly — we will discuss this on the proof complexity course mailing list.
  • Information about scribing and the scribing template files has been sent out on the course mailing list. If you are scribing, then please contact Jakob Nordström to be added to the scribing GitHub repository.

Short Overview

Simply put, proof complexity can be said to be the study of how to provide a short and efficiently verifiable certificate of the fact that a given propositional logic formula (typically in conjunctive normal form, or CNF) is unsatisfiable. Note that for satisfiable formulas there are very succinct certificates — just list a satisfying assignment — but for unsatisfiable formulas it is not quite clear what to do.

It is widely believed that it is not possible in general to give short certificates for unsatisfiable formulas, which if proven would imply P ≠ NP. One important research direction in proof complexity is to approach this distant goal by establishing lower bounds for stronger and stronger proof systems.

Another reason to study proof complexity is that any algorithm for deciding satisfiability of CNF formulas, or of related objects such as systems of polynomial equalities or linear inequalities, uses some method of reasoning to determine whether the sets of constraints in the input are feasible or infeasible. Studying the proof systems corresponding to these methods of reasoning and proving upper and lower bounds for them tells us something about the potential and limitations of such algorithms.

As indicated by the title above, this seminar course is mainly motivated by the second reason, and will therefore focus on proof systems that are especially interesting from an algorithmic perspective. We will introduce the proof systems resolution, Nullstellensatz, polynomial calculus, cutting planes, and Sherali-Adams — corresponding to SAT solving, algebraic reasoning, and geometric reasoning — survey some of the major research results, and present some open problems right at the research frontier. While the intention is to give a fairly broad coverage, there will be a slight bias towards topics where current and former members of the Mathematical Insights into Algorithms for Optimization (MIAO) group and our collaborators have made significant contributions to the state of the art.

Schedule and Course Contents

This course is given during the winter 2025/26. It is planned to have a total of 25-30 lectures, with two lectures per week on average.

In accordance with the academic quarter tradition, all times are stated cum tempore, so "13" in the lecture schedule below actually means "13:15". Regarding the length of the lectures, we will try to use some of the extra flexibility afforded between friends, going over two hours when the complexity of the materials requires it, but we will try not to use the full three hours in the schedule for each lecture.

Lectures in rooms starting with "E:" are at the CS department at Lund University at Klas Anshelms väg 10. We will be using the rooms E:2116, E:4121 "PaxLax2", E:2405 "Glasburen" (The Glass Cage), and E:3316 (where following the link will show a map of the E house with the location of the room). Abbreviations "VH <letter>" refer to meeting rooms <letter> on the ground floor at Vibenshuset at Lyngbyvej 2, where the Basic Algorithms Research Copenhagen (BARC) centre at the University of Copenhagen is currently located.

The intention is to stream all lectures on Zoom and post video recordings on the MIAO Research YouTube channel youtube.com/@MIAOresearch. Click on icons YouTube below to view available video recordings, or check out the YouTube playlist. Please contact Jakob Nordström to get information about the Zoom links used for the lectures.

Please note that the information below about what will be covered in future lectures is still somewhat tentative, since we might need to revise the planning slightly as we go along depending on what pace we manage to keep during the lectures.

 Weekday Date Time Room #  Plan of lectures References
 Thursday Oct 30 13-16 E:2116 1. Introduction to proof complexity as a computational lens YouTube [Nor15], [BN21], slides
 Tuesday Nov 4 13-16 E:4121 2. Proof complexity basics, resolution, and the pigeonhole principle YouTube [Hak85], [Pud00], slides, hand notes
 Thursday Nov 6 13-16 VH N 3. Resolution and Tseitin formulas YouTube [Urq87], hand notes, draft scribe notes
 Tuesday Nov 11 13-16 E:2405 4. Feasible interpolation for resolution YouTube [Pud97], hand notes, draft scribe notes
 Thursday Nov 13 13-16 VH L 5. Resolution and the clique problem YouTube [ABdR+21], hand notes
 Monday Nov 17 13-16 E:2116 6. Resolution and the clique problem (cont.) YouTube [ABdR+21], hand notes
 Tuesday Nov 18 13-16 E:2405 7. Resolution size-width lower bounds YouTube [IPS99], [BW01], draft scribe notes, hand notes
 Thursday Nov 20 13-16 VH Y 8. Nullstellensatz, polynomial calculus, and resolution YouTube [AR03], [MN24], hand notes
 Tuesday Nov 25 13-16 E:2405 9. A general method for polynomial calculus degree lower bounds: Applications YouTube [AR03], [MN24], hand notes
 Thursday Nov 27 13-16 VH Y 10. A general method for polynomial calculus degree lower bounds: Proofs YouTube [AR03], [MN24], hand notes
 Tuesday Dec 2 13-16 E:2405 11. Polynomial calculus and graph colouring [CdRN+23]
 Thursday Dec 4 13-16 VH L 12. Tightness of size-width/degree relations for resolution and polynomial calculus [Stå96], [BG01], [ALN16]
 Tuesday Dec 9 13-16 E:2116 13. Space complexity; resolution clause space vs. width [ABRW02], [AD08], [Ben09]
 Thursday Dec 11 13-16 VH L 14. Resolution space-width separation and size-space trade-offs [BN08], [BN11]
 Tuesday Dec 16 13-16 E:2116 15. Supercritical resolution size-space trade-offs [BBI16], [BNT13]
 Thursday Dec 18 13-16 VH L 16. Polynomial calculus space lower bound for random CNF formulas
 Thursday Jan 8 13-16 E:3316 17. Total space in resolution; polynomial calculus space vs. width/degree
 Friday Jan 9 13-16 E:3316 18. Size-degree trade-offs for Nullstellensatz and polynomial calculus
 Monday Jan 19 13-16 E:2116 19. Polynomial calculus and roots of unity encodings
 Tuesday Jan 20 13-16 E:2116 20. Cutting planes; more about feasible interpolation [Pud97]
 Thursday Jan 29 13-16 VH L 21. Cutting planes lower bounds for random CNF formulas
 Friday Jan 30 13-16 VH L 22. Size-space trade-offs for cutting planes
 Tuesday Feb 3 13-16 VH Y 23. Size-space trade-offs for cutting planes (cont.)
 Friday Feb 6 13-16 E:2405 24. Trade-offs for cutting planes with polynomially bounded coefficients
 Tuesday Feb 10 13-16 VH L 25. Lower bounds for cutting planes size from resolution width using lifting
 Friday Feb 13 13-16 E:2405 26. Lower bounds for cutting planes size from resolution width using lifting (cont.)
 Tuesday Feb 17 13-16 VH L 27. Automatability for resolution and polynomial calculus
 Friday Feb 20 13-16 E:2405 28. Final lecture; summary of material covered and outlook for future research

Lecturers

The main lecturer is Jakob Nordström. Jakob will be giving the lectures together with Kilian Risse, who will also help out with grading of problem sets and feedback on scribed lecture notes.

Course Goals

This seminar course is intended to:

  • give an introduction to proof complexity (partly with a view towards algorithmic connections),
  • survey some of the most recent exciting results in this area, and
  • present a number of open problems right at the frontier of current research,
so that that students after having completed the course will
  • have a good grasp of modern proof complexity (with a focus on proof systems corresponding to algoritms),
  • be able to reconstruct the proofs, at least in principle, of some of the major results during the last decades, and
  • be well equipped to attack open problems in the area (or will potentially already succesfully have done so).

Course Requirements

This seminar course is intended to give 7.5 ECTS credits.

The course examination will be by scribing notes for lectures (in LaTeX) and doing problem sets. More detailed information will be provided later.

Course Material

This course will mostly be based on research papers, and so there is no textbook. We plan to produce scribe notes from the lectures to help students study the material (and also use this scribing process as the main form of examination).

Below follow some information about resources that might be helpful.

Books and Surveys

The most recent comprehensive reference on proof complexity is a book titled (you guessed it) Proof Complexity by Jan Krajíček.

Some proof complexity surveys by the main lecturer, which have more of an algorithmic perspective on proof complexity, are:

Somewhat of a classic proof complexity survey is Propositional Proof Complexity: Past, Present and Future by Paul Beame and Toniann Pitassi. This paper is a bit dated by now, but it is still a very good read.

Research Articles

Please note that this section is being updated as we go along. In particular, we will try to make a more nicely and consistently formatted list of references below at some later point.

Below follows a fairly complete list of research articles on which the lectures are based. Note that for most of the papers we will only discuss a selection of the results, and the lectures are intended to cover the material in the articles that we need, so students are not required to read the papers listed below — the references are provided for completeness and for students interested in further reading. It should also be noted that many of the proofs given in class are actually not those found in the papers, and more recent survey papers of an area can sometimes be better reads than the original research articles. Please do not hesitate to talk to the lecturers if you are interested in specific references for some specific area.

Whenever available, links below are to the journal versions, which means that the date of the paper can sometimes be several years later than that of the original conference publication. For papers by the lecturers, the links are to personal PDF copies of the published papers rather than to publisher websites.

Scribe Notes

Information about scribing and scribe notes remains to be added.

Please note that these scribe notes are provided "as is" without warranty of any kind, either expressed or implied, including, but not limited to, the implied warranties of merchantability and fitness for a particular purpose. Having said that, the notes are of course intended to be as useful and correct as possible, so if you notice any errors or have any other suggestions for improvements (regardless of whether you are taking the course or just happen to visit this webpage), please do not hesitate to send an e-mail message to <jn~at-sign~di~dot~ku~dot~dk>.

Problem Sets

Part of the course examination will be by problem sets. The exact number of problem sets has not been decided, and depends on how many lectures the students will be required to scribe. As a rough guideline, fully scribing one lecture will count as the same amount of work as doing one problem set. Without any scribing, a course like this would normally have something like 4 problem sets.

Links to the problem sets will appear as they are being posted.

The actual deadlines for the problem sets are somewhat configurable, and can be discussed in class. The important thing is that we all agree on the deadlines beforehand, and that once they are set we stick to them without exceptions.

Problem Set Instructions

The following instructions apply for all problem sets.

  1. Please submit your solutions via e-mail as a PDF file. State your name and e-mail address close to the top of the first page. Solutions should be written in LaTeX or some other math-aware typesetting system with reasonable margins on all sides (at least 2.5 cm). Please try to be precise and to the point in your solutions and refrain from vague statements. Never just state an an answer, but make sure to also explain your reasoning. Write so that a fellow student of yours can read, understand, and verify your solutions.
  2. Submissions sohld be done on time. Note, however, that the submission deadline only specifies the date, and not the time zone. You are free to submit according to whatever time zone on earth you like, as long as the date in that time zone is correct.
  3. The intention from the instructor side is to grade and return submissions within two weeks.
  4. The thresholds for grading are stated on the first page of the problem set, and any adjustment of these thresholds will be communicated to students. (The thresholds can only be adjusted downwards and never upwards.)
  5. You are strongly encouraged to discuss the problem sets with other students, but you should write your own solution from scratch, and understand all details of them fully. It is not allowed to compose draft solutions together and then continue editing individually, or to share any text, formulas, or pseudocode. Also, no such material may be downloaded from the internet or generated via AI bots to be used in draft or final solutions.
  6. Some of the problems will be "classic" and hence their solutions can probably be found on the Internet or in research papers. It is not allowed to use such solutions in any way unless explicitly stated otherwise. Anything said during the lectures on in the lecture notes should be fair game, though, unless you are specifically asked to show something that we claimed without proof in class.

Other Proof Complexity Courses

Below you find webpages for some other recent (and not-so-recent) courses on proof complexity as given by:

(There are other proof complexity courses out there as well that your favourite search engine can find for you, but the ones listed above are probably those that are closest to our interests.)

Published by: Jakob Nordström <jn~at-sign~di~dot~ku~dot~dk>
Updated 2025-11-27