There certainly are such proofs. Even for simple decidable theories we have very large lower bounds on decision complexity (like double exponential), which implies large lower bounds on the function from "length of theorem statement" to "length of shortest proof".

For undecidable theories, there is no computable function bounding this blowup from theorem length to proof length (otherwise, the theory would be decidable.)