In some areas of mathematics it is everyday practice to prove the existence of things by entirely non-constructive arguments that say nothing about the object in question other than it exists, e.g. the celebrated probabilistic method and many things found in this thread: What are some things we can prove they must exist, but have no idea what they are?
Now what about proofs themselves? Is there some remote (or not so remote) area of mathematics or logic which contains a concrete theorem that is actually capable of being proved by showing that a proof must exist without actually giving such a proof?
Naively, I imagine that this would require formalizing a proof in such a way that it can be regarded as a mathematical object itself and then maybe showing that the set of such is non-empty. The only thing in this direction that I've seen so far is the "category of proofs", but that's not the answer.
This may sound like mathematical science fiction, but initially so does e.g. the idea of proving that some statement is unprovable in a framework, which has become standard in axiomatic set theory.
Feel free to change my speculative tags.
Best Answer
There are various ways to interpret the question. One interesting class of examples consists of "speed up" theorems. These generally involve two formal systems, $T_1$ and $T_2$, and family of statements which are provable in both $T_1$ and $T_2$, but for which the shortest formal proofs in $T_1$ are much longer than the shortest formal proofs in $T_2$.
One of the oldest such theorems is due to Gödel. He noticed that statements such as "This theorem cannot be proved in Peano Arithmetic in fewer than $10^{1000}$ symbols" are, in fact, provable in Peano Arithmetic.
Knowing this, we know that we could make a formal proof by cases that examines every Peano Arithmetic formal proof with fewer than $10^{1000}$ symbols and checks that none of them proves the statement. So we can prove indirectly that a formal proof of the statement in Peano Arithmetic exists.
But, because the statement is true, the shortest formal proof of the statement in Peano Arithmetic will in fact require more than $10^{1000}$ symbols. So nobody will be able to write out that formal proof completely. We can replace $10^{1000}$ with any number we wish, to obtain results whose shortest formal proof in Peano arithmetic must have at least that many symbols.
Similarly, if we prefer another formal system such as ZFC, we can consider statements such as "This theorem cannot be proved in ZFC in fewer than $10^{1000}$ symbols". In this way each sufficiently strong formal system will have some results which we know are formally provable, but for which the shortest formal proof in that system is too long to write down.