<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">REMINDER:</font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class=""><br class=""></font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">Department of Mathematics & Computer Science</font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">Combinatorics & Theory Seminar</font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class=""><br class=""></font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">Tuesday, October 29, 2019</font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">Ryerson 251@ 3:30 pm</font></b></div><div class=""><font face="TimesNewRomanPSMT" size="4" class=""><br class=""></font></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">Mika Goos</font></b></div><div class=""><b class=""><font face="TimesNewRomanPSMT" size="4" class="">IAS</font></b></div><div class=""><div class=""><font face="TimesNewRomanPSMT" size="4" class=""><br class=""></font></div><div class=""><font face="TimesNewRomanPSMT" size="4" class=""><b class="">Title:</b> Automated Proof Search: The Aftermath<br class=""><br class=""><b class="">Abstract:</b><br class="">In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper)<br class="">settled the complexity of finding short proofs in Resolution, the most basic<br class="">propositional proof system. Namely, given an unsatisfiable CNF formula F, they<br class="">showed it is NP-hard to find a Resolution refutation of F in time polynomial in<br class="">the length of the shortest such refutation.<br class=""><br class="">In this talk, we present a simple proof of the Atserias--Muller theorem.<br class="">The new proof generalises better: We obtain analogous hardness results for<br class="">Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work)<br class="">Cutting Planes. An open problem is to include Sum-of-Squares in this list.<br class=""><br class="">Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann<br class="">Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.<br class=""></font></div><div class=""><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;"><font class="" face="TimesNewRomanPSMT" size="4"><br class=""></font></div><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;"><font class="" face="TimesNewRomanPSMT" size="4">Host: Prof. Aaron Potechin</font></div></div></div></div></div></div></div><div class=""><div class="" style="text-align: -webkit-auto; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; orphans: 2; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;"><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;" class=""><font face="TimesNewRomanPSMT" size="4" class=""><br class="webkit-block-placeholder"></font></div><div class="" style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;"><div class=""><font face="TimesNewRomanPSMT" size="4" class="">Refreshments will be served during the talk</font></div></div></div></div></div></div></div><div class=""><div style="text-align: -webkit-auto; font-family: Helvetica; font-size: inherit; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; orphans: 2; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;" class=""><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto; font-size: 11px;" class=""><br class="webkit-block-placeholder"></div><div style="font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; text-align: -webkit-auto;" class=""><br class="webkit-block-placeholder"></div></div></div></div></div></div><div class="">
<div style="color: rgb(0, 0, 0); font-family: Helvetica; font-size: inherit; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; font-size: 11px;" class=""><br class="webkit-block-placeholder"></div><div style="color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-east-asian: normal; font-variant-position: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div class=""><p class="MsoNormal" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; text-decoration: none; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal;"><b class=""><font size="4" class="">Donna Brooms-Blue</font></b></p><br class="Apple-interchange-newline" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; text-decoration: none;"></div>
</div></div></div></div></div></div><br class=""></div></div></div></div></body></html>