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

Computer Science/Discrete Mathematics Seminar II
Topic:Short proofs are hard to find (joint work w/ Toni Pitassi and Hao Wei)
Speaker:Ian Mertz
Affiliation:University of Toronto
Date:Tuesday, December 5
Time/Room:10:30am - 12:30pm/S-101

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.