A fertile area of recent research has found concrete polynomial time lower bounds for solving hard computational problems on restricted computational models. Among these problems are Satisfiability, Vertex Cover, Hamilton Path, MOD6-SAT, and Majority-of-Majority-SAT, to name a few. The proofs of such lower bounds all follow a certain proof-by-contradiction strategy. I will survey some of the results in this area, giving an overview of the techniques involved. If there is time I will discuss an automated search strategy for studying these proof techniques. In particular, the search for better lower bounds can often be turned into the task of solving a large series of linear programming instances. Furthermore, the limits of these proof system(s) can be understood by analyzing the space of possible linear programs