Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is actually to find the proof? When I say "substantially easier," the tediousness of formalizing an informal proof should not be considered. In other words, a rigorous but informal proof doesn't count as a nonconstructive demonstration that a formal proof exists, since there is no essential difficulty in producing a formal proof besides workload. If there is some essential barrier, then there's something wrong either with the proof or with the definition of "formal proof." (Although the concept of "informal proof" is by nature vague, it seems reasonable to say that the procedure transforming a typical informal proof to a formal proof is a primitive recursive computation, even though it's probably impossible to make that precise enough to prove.)
I don't know what such a nonconstructive meta-proof could look like, but I also don't see why one couldn't exist. The only near-example I can think of right now is in the propositional calculus: you can prove that a propositional formula is a theorem by checking its truth table, which does not explicitly provide a deduction from the axioms; however, in most interesting cases, that probably isn't much easier (if at all) than exhibiting a proof, just maybe more mechanical. (Of course, estimating the difficulty of proving or disproving a candidate for a propositional theorem is a huge open problem.) Also, I think there is actually a simple way to convert a truth-table proof into an actual deduction from the axioms of propositional calculus, although I don't remember and didn't retrace all of the details. (Anyway, I'm not even so interested in the propositional calculus for this question, since it's not very expressive.)
Another thing that seems vaguely relevant is Godel's completeness theorem, which states that a formula is a theorem of a first-order theory if and only if it is true in every model of that theory. I don't know in what cases it would be easier, though, to show that some formula were true in every model than it would be just to prove the theorem in the theory.
Best Answer
Set theory provides a good example. It is often convenient in set theory to work with the concept of "classes" and treat them as mathematical objects of their own kind. The standard axiomatization of set theory with classes is called Goedel-Bernays set theory, denoted GBC, whereas the usual ZFC axioms have only set objects. But there is a general theorem that any statement purely about sets that is proved by using classes in GBC can be proved without them purely in ZFC. This is what it means to say that GBC is a conservative extension of ZFC. To prove this general theorem, it suffices to observe that any ZFC model can be expanded to a model of GBC, by adding only the classes definable from parameters.
There are many other examples of conservative extensions in mathematics, and all of them would seem to be examples of the type that you seek. For example, PA has a conservative extension to the analogous theory true in the collection HF of hereditarily finite sets. Thus, to prove a theorem about numbers in PA, one can freely use heredtiarily finite sets (e.g. sequences of numbers, sequences of sets of numbers, etc.), not just as coded by numbers via Goedel coding, but as actual mathematical objects. And surely this makes proofs much easier.
Perhaps another type of example arises in the absoluteness phenomenon in set theory. For example, the Shoenfield Absoluteness theorem states that any Sigma^1_2 statement has the same truth value in any two models of set theory with the same ordinals. In particular, to prove that a particular Sigma^1_2 statement is true in ZFC, it suffices to prove it under the assumption also that V=L, where one also has all kinds of additional structure available. The Absoluteness Theorems (and there are many) can therefore be viewed under the rubric you mention.
But of course, in all these cases, we have an actual proof in the weaker theory. To prove that there is a proof, is a proof, so I believe ultimately there will be no way to avoid the quibbling over whether it is easy or hard to translate the high-level proof into a low level proof, since in principle it will always be possible to do this.