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.

Date

Speakers

Ian Mertz

Affiliation

University of Toronto

Files & Media