Establishing that minimal proofs (or "derivations") of certain statements or theorems are long, is the prime target of the area called *proof complexity*. 
Concerning examples given in prior answers, like Haken's size lower bound on proofs of the pigeonhole principle, they deal with **propositional logic** only. Therefore, they are *asymptotic* results of the form: "there exists a constant $ 0<\epsilon<1 $ such that any resolution refutation of the propositional pigenohole principle $ PHP_n$ must be of length (i.e., number of steps) at least $ 2^{n^\epsilon}$"; Where $ PHP_n \;$,  $ n=1,2,\ldots ,$  is an infinite family of propositional contradictions (expressing the pigeonhole principle). So propositional proof complexity does not seem to answer the question about non-asymptotic lower bounds.

On the other hand, lower bounds on *first order* proofs (having quantifiers, i.e., not propositional logic) are not necessarily asymptotic, and if this is what you are looking for, the only thorough survey I know of (dealing with both propositional and non-propositional) proof complexity is:  *Pavel Pudlak: The lengths of proofs, in Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637*, available [here][1]

(There is also an older book by Orevkov on non-propositional proof complexity: [1993] Complexity of Proofs and Their Transformations in Axiomatic theories, vol. 128 of
Translations of Mathematical Monographs, American Mathematical Society, Providence,
Rhode Island.)

  [1]: http://www.math.cas.cz/~pudlak/length.pdf