
One of the main motivations for proof complexity is meta-mathematics: understanding how hard mathematical theorems are to prove. In complexity theory, we are especially motivated to understand the meta-mathematics of complexity lower bounds, and therefore meta-complexity is obviously relevant here. This workshop will focus on questions such as: Are there further barriers to lower bounds beyond the natural proofs, relativization, and algebrization barriers? What formal connections can we show between proof complexity and circuit complexity, and what does this imply for the meta-mathematics of circuit lower bounds? What is the strongest propositional proof system for which we can show that all truth table tautologies are hard? Is bounded-depth Frege hard to automate? Is there a formal connection between learning and automatability?