In "Finding Efficient Circuits Using SAT-solvers", Kojevnikov, Kulikov, and Yaroslavtsev have used SAT solvers to find better circuits for computing $MOD_k$ function.
I have used computers to find proofs of time-space lower bounds, as described here. But that was only feasible because I was working with an extremely restrictive proof system.
Maverick Woo and I have been working for some time to find the "right" domain for proving circuit upper/lower bounds using computers. We had hoped that we may resolve $CC^0$ vs $ACC^0$ (or a very weak version of it) using SAT solvers, but this is looking more and more unlikely. (I hope Maverick doesn't mind me saying this...)
The first generic problem with using brute-force search to prove nontrivial lower bounds is that it just takes too damn long, even on a very fast computer. The alternative is to try to use SAT solvers, QBF solvers, or other sophisticated optimization tools, but they do not seem to be enough to offset the enormity of the search space. Circuit synthesis problems are among the hardest practical instances one can come by.
The second generic problem is that the "proof" of the resulting lower bound (obtained by running brute-force search and finding nothing) would be insanely long and apparently yield no insight (other than the fact that the lower bound holds). So a big challenge to "experimental complexity theory" is to find interesting lower bound questions for which the eventual "proof" of the lower bound is short enough to be verifiable, and interesting enough to lead to further insights.