Computational cost of extracting a proof Suppose we are studying the Zermelo–Fraenkel set theory as a first-order logic and our metatheory is also the Zermelo–Fraenkel set theory.
Is there a statement $P$ such that

*

*no direct proof of $P$ has ever been written down

*but an algorithm has been formulated in the metatheory that has been shown to terminate and has been shown to output a valid proof of $P$?

EDIT: as pointed out by Emil Jeřábek if one assumes $\Sigma_1$-soundness then a variant of "this statement cannot be proven in fewer than a googol symbols" works. Ideally I would like an example where $\Sigma_1$-soundness/consistency is not assumed.
 A: For every concrete natural number $n$, $\mathsf{ZFC}$ proves the consistency of the subset, let's call it $\mathsf{ZFC}_n$, of the axioms of $\mathsf{ZFC}$ where the axiom scheme of Replacement is restricted to $\Sigma_n$ predicates: this follows from standard arguments around the reflection principles (there exists a $V_\alpha$ which reflects any finite number of formulas of set theory, and furthermore, $\Sigma_n$-replacement can be written as a single statement).  Let $\mathrm{Consis}(\mathsf{ZFC}_n)$ be the statement in question (that $\mathsf{ZFC}_n$ is consistent): then

*

*“$\mathrm{Consis}(\mathsf{ZFC}_n)$” is a theorem of $\mathsf{ZFC}$ for every $n$; this fact is a theorem of, say, Peano arithmetic, and furthermore, there exists an explicit algorithm which, given $n$, produces a proof of $\mathrm{Consis}(\mathsf{ZFC}_n)$ in $\mathsf{ZFC}$ (the “standard arguments” I alluded to),


*but of course, by Gödel's incompleteness theorem, “$\forall n. \mathrm{Consis}(\mathsf{ZFC}_n)$”, which is just $\mathrm{Consis}(\mathsf{ZFC})$ by compactness) cannot be a theorem of $\mathsf{ZFC}$ if $\mathsf{ZFC}$ is consistent, in other words, the proof cannot be made uniform within $\mathsf{ZFC}$.
So for $n$ large enough, $\mathrm{Consis}(\mathsf{ZFC}_n)$ is an example of what you are asking for: its proof has never been explicitly written down within $\mathsf{ZFC}$, only as a template algorithm which demonstrably produces a proof for any given $n$, yet it's not a trivial matter of instancing a single uniform proof¹ because no single uniform proof exists.

*

*I mean, it's not like something like $n+1=1+n$ which is obviously provable for each $n$ and for many $n$ the proof has never been written down yet we have an algorithm which produces it by applying the proof of $\forall n.(n+1=1+n)$ to that particular $n$ (this formally answers your question, but obviously you want more than that): in my above example, you simply cannot make the proof uniform, because Gödel's theorem prevents it.

A: This is a suggested clarification of the question; judging from the responses, I think the question is not completely clear.  [EDIT: Under the assumption that this clarification is correct, an answer to the question is given below.]
The intended question, I believe, is something like this.  If there is a short ZF proof of "ZF proves P" then is there necessarily a short ZF proof of P?  If not, then can we write down an explicit example of a short ZF proof of "ZF proves P" for which it is infeasible to write down an explicit ZF proof of P?
The first thing to note is that there need not be a ZF proof of P at all, unless we assume some kind of soundness condition on ZF.  For example, suppose P is the statement 1=0.  We don't know a way of deducing the inconsistency of ZF from the assumption that ZF proves "ZF is inconsistent."  Now, this observation does not torpedo the question, because if someone explicitly writes down a ZF proof of "ZF proves P" then we are all going to be convinced both that ZF proves P and that P.  But it does show that passing from a proof of "ZF proves P" to a proof of P is not entirely trivial.
The second observation is that examples involving infeasibly large P do not really answer the intended question.  We are, I think, supposed to fix some straightforward algorithm for converting P into "ZF proves P".  In particular, if P is infeasibly large then "ZF proves P" will be infeasibly large, so that writing down an explicit proof of "ZF proves P" will be infeasibly large.  What is being asked is, how much of a blowup in proof size can there be when passing from "ZF proves P" to P itself?

EDIT (based on   Emil Jeřábek's comments below): Suppose we interpret the phrase "has been shown" as permitting us to assume that ZF is $\Sigma_1$-sound. Then, as explained in the comments below, we can take some fast-growing recursive function $f$ (Ackermann, say), and let $P$ be the following "self-referential" statement:

There exists $x$ such that there is a ZF-proof of $\mathsf{Prov}(P)$ of length at most $x$ but no ZF-proof of $P$ of length at most $f(x)$.

Since $P$ is $\Sigma_1$, one can explicitly construct a relatively short ZF-proof of $\mathsf{Prov}(P)$.  If we now assume that ZF is $\Sigma_1$-sound, then we can conclude that $P$ is true, so that means that the "trivial" algorithm that searches for a proof of $P$ will terminate with a valid proof of $P$.  However, the shortest such proof will be infeasibly long and hence has never been (and never will be) written down explicitly.
If the assumption that ZF is $\Sigma_1$-sound bothers you, then you can try carrying out the following thought experiment.  Imagine yourself following the above recipe and explicitly constructing the ZF-proof of $\mathsf{Prov}(P)$.  Imagine yourself reading through this ZF-proof line by line.  Presumably, reading and understanding a ZF-proof of something convinces you that it is true, so at the end of this process, you will become convinced that $P$ is in fact provable in ZF.  Now you have to decide for yourself whether the ZF-provability of $P$ "has been shown."
A: [This is more an overly long comment than a proper answer.]
There is a formal ZF-proof for a theorem $T$, if and only if the algorithm that generates all potential ZF-proofs, checks whether they are for $T$ and halts if the answer is ever "yes" terminates. Thus, as long as we use the usual standards for "proof" in mathematics, the distinction from the question doesn't really make sense.
Since we hardly ever write down formal ZF-proofs for stuff, the answer quite certainly is "no" if we read "known proof" as "someone has explicitly written down a formal ZF-proof" - but for boring reasons.
To get somewhere interesting, we might ask whether there is an instance of a theorem $T$ where the shortest explicit formal ZF-proof is signficantly longer than the combination of a program and a formal ZF-proof that the program would halt and output a formal ZF-proof of $T$.
If we only count the length of the program and the proof that it terminates, but keep the proof that the output indeed is a formal ZF-proof of $T$ separate, then the answer is clearly "yes", and we can do this for almost all theorems. Here, we just add to our exhaustive proof search algorithm from above a sufficiently big length cutoff. The termination proof is trivial, and the program itself has size constant +  Kolmogorov complexity of $T$ + Kolmogorov complexity of the size of the shortest proof of $T$, which generally be less than the size of the shortest proof itself.
A: Not really my area of expertise, but I think that the answer to your question is no.
If you could prove the existence of an algorithm for proving $P$ and prove that
the algorithm terminates and that the proof it produces is valid, then you
have proven that $P$ is true, i.e., is a theorem of ZFC.  Even if the proof is
meta-theoretic, it could be formalized in ZFC to produce a proof of $P$ that is
shorter than the one produced by its algorithm.
The problems referenced above (by @Wojowu) are ones for which we can prove that either $P$ or
$\lnot P$ is a ZFC theorem, so they are not independent statements like CH.  For
any such statement, there is an algorithm for deciding $P$: just write a program
that enumerates all the theorems of ZFC and wait for either $P$ or $\lnot P$ to
appear.  The problem, of course, is that the time required might be
intractable.
On the other hand, there certainly exist theorems of ZFC for which the
shortest possible proof requires an intractably large number of steps, say
$10^{110}$.  This number exceeds the number of nanoseconds in 14 billion years
multiplied by the number of atoms in the universe.  So, if you could convert
every atom of the universe to a Gigahertz computing device, then travel back
to the beginning of time and start this computing system, it would not yet
have completed $10^{110}$ operations.
It is entirely possible that, for example, $P\ne NP$ is such a theorem.  If so,
the Clay Institute's million dollars is safe :-).
