Proof complexity, the study of the lengths of proofs in
propositional logic, is an area of study that is fundamentally connected
both to major open questions of computational complexity theory and
to practical properties of automated theorem provers. In the last
decade, there have been a number of significant advances in proof
complexity lower bounds. Moreover, new connections between proof
complexity and circuit complexity have been uncovered, and the interplay
between these two areas has become quite rich. In addition, attempts
to extend existing lower bounds to ever stronger proof systems of proof
have spurred the introduction of new and interesting proof systems,
adding both to the practical aspects of proof complexity as well as
to a rich theory.

This note attempts to survey these developments
and to lay out some of the open problems in the area.
This is an updated version of our article appearing in
the Computational Complexity Column of the Bulletin of
the EATCS, 1998.