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.