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 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
(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.)