In 1936 Gödel announced a theorem to the effect that proofs of certain theorems $T_1,T_2,\ldots$ become dramatically shorter when one passes from a formal system, such as Peano arithmetic PA, to a stronger one, such as a system in which Con(PA) is provable. More precisely, given any computable function $f$, we can find a sequence $T_1,T_2,\ldots$ of theorems such that $T_k$ has a proof of length of order $k$ in the stronger system, whereas any proof of $T_k$ in PA has length at least $f(k)$.
Various versions of this theorem have been proved, depending on the strengthening of PA chosen, and on the definition of length. See, in particular, this paper. However, I have not found a version with a
natural sequence of theorems $T_k$. For example, it seems plausible that one could use Goodstein's theorem, by taking
$T_k$ = The Goodstein process, starting with input $k$, eventually halts.
Are any such "natural'' examples of Gödel speed-up known?
Update and clarification. Gödel's speed-up theorem gives, for any computable function $f$, a sequence
of theorems $T_1,T_2,\ldots$ of PA such that each $T_k$ has a proof of length $O(k)$ in some strengthening of PA,
while the shortest proof of $T_k$ in PA has length $\ge f(k)$. In this theorem, the sequence $T_1, T_2,\ldots$
depends on $f$.
If we want a "natural" sequence $T_1,T_2,\ldots$ (in particular, if $T_k=\varphi(k)$ for some fixed formula $\varphi$)
then we can no longer demand that $f$ be an arbitrary computable function, or even of arbitrary computable rate of
growth. This is because (assuming the sequence $T_1,T_2,\ldots$ is c.e.) the function
$g(k)$ = length of the shortest proof of $T_k$ in PA
is computable, so we cannot ask $f$ to grow faster then $g$.
So, since I want the sequence $T_1,T_2,\ldots$ to be fixed, I have to be satisfied if $T_k$ has shortest proof in PA
with length of $O(f(k))$ some reasonably fast-growing $f$. It seems that Harvey Friedman has examples that fit the
bill, as Richard Borcherds has pointed out. However, before I accept Richard's answer, I would like to know a precise
reference. I have pored over Harvey Friedman's Research on the Foundations of Mathematics (North-Holland 1985),
and some other works, without finding a clear statement of speed-up in the above sense.
Best Answer
Friedman has given many examples of such speedups. One well known one is his finite version of Kruskal's tree theorem. In particular he gave examples of reasonably natural statements that have very short proofs in 2nd order arithmetic, and can be proved in Peano arithmetic, but the shortest proof in Peano arithmetic is ridiculously long.