Abstract
For several years, both proof complexity and practical solving focused on propositional proof systems and detecting (un)satisfiability. In the last two decades, several proof systems for the more succinct Quantified Boolean Formulas QBFs have been proposed and studied, and several QBF solvers have been developed. This talk will give an overview of what has been achieved in QBF proof complexity and how (if at all) it informs QBF solving, and will hopefully include some speculative discussion about future directions.