January 28 – February 2 , 2018, Dagstuhl Seminar 18051

Proof Complexity


Albert Atserias (UPC – Barcelona, ES)
Jakob Nordström (KTH Royal Institute of Technology – Stockholm, SE)
Pavel Pudlák (The Czech Academy of Sciences – Prague, CZ)
Rahul Santhanam (University of Oxford, GB)

For support, please contact

Annette Beyer for administrative matters

Andreas Dolzmann for scientific matters


List of Participants
Shared Documents
Dagstuhl Seminar Wiki
Dagstuhl Seminar Schedule (Upload here)

(Use seminar number and access code to log in)


The study of proof complexity was initiated by Cook and Reckhow in 1979 as a way to attack the P vs. NP problem, and in the ensuing decades many powerful techniques have been discovered for understanding different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are when measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables.

During the last 10-15 years the area of proof complexity has seen a revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent progress gives hope that the area may be ripe for decisive breakthroughs.

In this Dagstuhl Seminar, we aim to bring together leading experts covering the whole spectrum of proof complexity from Frege proof systems and circuit-inspired lower bounds via geometric and algebraic proof systems all the way to bounded arithmetic, as well as prominent researchers from neighbouring fields. We hope and believe that such a seminar could have a major impact at this critical juncture. Besides the regular program including talks about recent research results, we plan to organize open problem sessions, and expect ongoing research discussions throughout the week in smaller groups.

  Creative Commons BY 3.0 DE
  Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam


  • Data Structures / Algorithms / Complexity
  • Verification / Logic


  • Proof complexity
  • Computational complexity
  • Logic
  • Bounded arithmetic
  • Satisfiability algorithms

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support