SAS

Abstract

I will discuss a recent result proved with Yuval Filmus and Toni Pitassi: exponential size lower bounds for constant-depth Frege imply superpolynomial size lower bounds for Frege. The proof is constructive in that it shows how to simulate polynomial size Frege proofs for any sequence of tautologies with sub-exponential size proofs in constant-depth Frege. The simulation is tight for tree-like proofs. I will also mention consequences of the result for weak automatizability of constant-depth Frege.