Abstract
There are many fascinating connections between proofs and circuits, between efficient provability and efficient computability. In this talk, I will focus on two of these: the feasible interpolation method formulated by Krajicek in the early 90's and some of the lifting theorems that have flourished in the last few years. The former, for example, implies that the clique-coloring principle is hard to prove (in resolution) because clique-coloring is hard to compute (by monotone Boolean circuits); and the latter implies that clique-coloring is hard to compute (by monotone Boolean circuits) because the pigeonhole principle is hard to prove (in resolution).