If we search for the proof of a theorem then, assuming that there exists a proof, it lies in the set of all proofs of all provable theorems. But since this set is infinite, this means that the shortest length of the proof can be arbitrarily large. Almost all provable theorems will thus have a minimum proof length that exceed our ability to find them by some arbitrary large margin.
How can we then explain the fact that there are many proven theorems in mathematics? These theorems cannot be typical theorems, but what makes them atypical that makes their proofs to be short?
There are three problems with this question. First is the jump from the second sentence to the third. While it is true that the length of a proof can be large, that does not show that there are theorems that have a very long shortest possible proof. I believe it, but there is no proof here and I do not find it obvious. We could just fiddle around as long as we want, then prove the theorem. The second is that we can make complicated theorems by compounding simpler unrelated ones. If we have one theorem that takes $m$ steps to prove and another unrelated one that takes $n$ steps to prove, their conjunction takes $m+n+1$ steps to prove, but we haven't really learned anything new when we do that. The third, and I think the largest, is that the existence of hard theorems does not say anything about whether there are easy interesting theorems. Whether they are typical is not important. You can prove the Pythagorean theorem in a few dozens of lines, but it is important and interesting. The fact that there are theorems in Euclidean geometry that we have not found yet does not change that. Neither does the fact that it is not typical of the length of the "average theorem" (however you define that).