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.