Abstract
This talk will be a partial survey of the efforts that, over the years, proof complexity theorists have put into finding hard instances for SAT and other computational problems. Hopefully, the picture that will emerge is that one of the goals of this search is, paradoxically, to discover new and better algorithms.