It's interesting that it seems that some very short propositions require very long proofs. Are there any results on the length (or maybe Kolmogorov complexity)

It's interesting that it seems that some very short propositions require very long proofs. Are there any results on the length (or maybe Kolmogorov complexity) of the shortest proof for provable propositions of length N? (in a specific logic system, I suppose) I.e. how hard to prove is the hardest proposition of length of N and how does it grow with N? how about the average random provable proposition?