I ran across this discussion by Daniel Shanks,

"Is the quadratic reciprocity law a deep theorem?." Solved and Unsolved Problems in Number Theory. Vol. 297. AMS, 2001. p.64ff.

which made me wonder:

Q. Is there a theorem in some formal system whose proofs are known to be necessarily "long" in some sense, perhaps in the Kolmogorov-complexity sense?

I know it has been established that there are relatively "short" theorems that have only enormously "long" proofs (apparently[?] due to Gödel,"On the length of proofs"), but I'm asking if it is known that some particular theorem only has long proofs? (This is in some sense the obverse of the MO compendium, "Quick proofs of hard theorems.")

Obviously this is a naive question!