Short proofs are hard to find (joint work w/ Toni Pitassi and Hao Wei)

Proof complexity studies the problem computer scientists and mathematicians face every day: given a statement, how can we prove it? A natural and well-studied question in proof complexity is to find upper and lower bounds on the length of the shortest proof of a given tautology in a given proof system, and from those bounds gain insight into how powerful the proof system may be. Another natural yet less understood question is to efficiently find such a short proof for the tautology. From this problem, known as automatizability, we can hope to understand not just the expressiveness of a proof system but also its practicality.

In this talk I first survey the landscape of proof complexity and known automatizability results in well-studied proof systems, including the important result of Alekhnovich and Razborov who prove that the Resolution system is not automatizable. I will then present a self-contained, simplified, and quantitatively stronger proof of the AR theorem, and discuss extensions of the proof to to other proof systems, as well as limitations and open problems.