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.