If you're willing to accept a contrived statement, then it's not hard to get an explicit example, but this may not be the sort of example you're looking for.

Following Gödel's approach, you can make a statement of the form "I have no formal proof of less than a hundred pages." (More precisely, you should use implicit self reference, along the lines of "There is no formal proof of less than a hundred pages for this string followed by its quotation: 'There is no formal proof of less than a hundred pages for this string followed by its quotation:'")

Assuming your formal system is consistent, this statement cannot be proved in less than a hundred pages. In that case it actually is provable, because you can prove it by enumerating all possible proofs of less than a hundred pages and checking that they don't work. Thus, we have a relatively short theorem that has no short formal proof. Sadly, the theorem is of no intrinsic interest.

Note that the reason it didn't take us a hundred pages to prove the theorem is because we assumed the formal system was consistent. By Gödel's second incompleteness theorem, the system can't prove its own consistency, so this approach is not available within the system. In fact, this argument proves the second incompleteness theorem: if consistency had a short enough proof, then we could carry out this argument to prove the theorem in under a hundred pages. There's nothing special about a hundred pages in this argument, so there can be no proof of consistency at all. This approach to the second incompleteness theorem is fundamentally the same as Gödel's original proof.

Here I've been measuring proofs by length, rather than the Kolmogorov complexity mentioned in the question. That's not a useful measure for proofs, because you can reconstruct the shortest proof of theorem X in system S from little more than X and a proof checker for S (which you apply to do a brute force search for the shortest proof). This means if you fix S, the Kolmogorov complexity of the shortest proof is no more than an additive constant greater than that of the theorem itself.

1more comment