Abstract
I will describe the state-of-the-art in proof complexity lower bounds achieved via reductions to algebraic circuit lower bounds. We shall see that in the world of algebraic proof systems, when not insisting that hard instances are in CNF, major problems that are open in the corresponding world of boolean (Frege-style) systems, are already solved. I'll present some open problems and directions for further study, including barriers to obtaining CNF hard instances (which would solve major open problems in proof complexity).