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.
Best Answer
This is a commonly misunderstood aspect of constructive mathematics. The constructive method to prove "there does not exist an object with property $P$" is to assume there is an object with property $P$ and derive a contradiction.
For example, this is a constructive proof:
This is because, in the constructive reading, the actual meaning of "not X" is "X implies a contradiction" -- "not X" is really an implicational statement. One thus proves a statement of the form "not X" in the same way that one proves any other implication.