Proof complexity is a vibrant area in the intersection of computational complexity, algorithms and mathematical logic exploring the inherent difficulty of proving mathematical theorems. This workshop aims to cover both traditional topics and emerging trends in the field such as lower bounds on lengths of proofs, bounded arithmetic, model theory & forcing, SAT & QBF solving, connections to TFNP and algebraic complexity, lifting theorems and meta-mathematics of complexity theory.

The workshop will take place on 3-5 September at the University of Oxford. The program will consist of talks by selected speakers and will include ample time for discussions. The registration for the workshop is now closed, but if you have access to the building, you are welcome to participate.

Program:

Tuesday

10:00 - 10:30 coffee break

10:30 - 11:30 Robert Robere 

Proof complexity, pigeonhole principles, and total search problems

11:30 - 14:00 lunch

14:00 - 14:50 Hanlin Ren 

Meta-mathematics of Resolution lower bounds: A TFNP perspective

14:55 - 15:25 Igor C. Oliveira 

Hardness of near-optimal indistinguishability obfuscation (and connections to metacomplexity and bounded arithmetic)

15:30 - 16:00 coffee break

16:00 - 16:25 Dimitrios Tsintsilidas 

Provability of the Circuit Size Hierarchy and its consequences

16:30 - 16:55 Fedor Part 

Towards Res(lin) lower bounds over finite fields: error correcting codes

Wednesday

10:00 - 10:30 coffee break

10:30 - 11:10 Pavel Pudlák

Proofs, games, circuits, TFNP, and communication complexity

11:15 - 11:55 Dmitry Sokolov 

One more supercritical tradeoff for Resolution

12:00 - 14:00 lunch

14:00 - 14:50 Kilian Risse 

Clique is hard on average for Sherali-Adams with bounded coefficients

14:55 - 15:20 Svyatoslav Gryaznov 

Bounded depth Frege lower bounds for random 3-CNFs via deterministic restrictions

15:30 - 16:00 coffee break

16:00 - 16:25 Ilario Bonacina 

MaxSAT Resolution with Inclusion Redundancy

16:30 - 16:55 Anastasia Sofronova 

Disjunction of AC^0 over different F_2^n-bases

Thursday

10:00 - 10:30 coffee break

10:30 - 11:30 Moritz Müller 

Forcing in bounded arithmetic

11:30 - 14:00 lunch

14:00 - 14:25 Emil Jeřábek 

Towards analysis in VTC^0

14:30 - 14:55 Noel Arteche

Quantum automating TC^0-Frege is LWE-hard

15:00 - 15:25 Erfan Khaniki 

From proof complexity to circuit complexity via interactive protocols

15:30 - 16:00 coffee break

16:00 - 16:25 Sasank Mouli 

Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

16:30 - 16:55 Artur Riazanov

Hardness condensation by restriction