How fast does the Godel speed-up theorem proof length grow? Godel's speed-up theorem states that are theorems with arbitrarily long proofs (and can be arbitrarily shortened by working in a more powerful system).
Let $g(n)$ be defined as the number of symbols in the shortest proof of "This statement cannot be proved in Peano Arithmetic in less than n symbols"
$g(n)=\Omega(n)$, since any proof of the statement for $n$ would lead to a contradiction in PA.
$g(n)=\mathcal O (e^n)$, since you can proof the $n$th statement by simply listing all proofs under $n$ symbols (of which there are exponentially many) and noting that none of them prove the statement (and we established that none of them do since they would lead to an inconsistency in PA). This argument in particular means that $g(n)$ is defined for all $n$.
So the growth rate of $g$ lies between linear and exponential. Can we more precisely pinpoint its growth rate? (For example, could we say that $g(n)=\Theta(n^x)$ for some $x$?)
 A: It is possible to show that $g(n)=n^{\Theta(1)}$. This result essentially is due to Pavel Pudlák [1]. Below I'll sketch how this could be proved.
The sentence $\varphi_n$="This statement cannot be proved in Peano Arithmetic in less than n symbols" is a finite analogue of Gödel's fixed-point $\varphi\leftrightarrow \lnot\Box\varphi$ (here $\Box\varphi$ is a shorthand for "$\mathsf{PA}$ proves $\varphi$"). Recall that the main part of the standard proof of Gödel's 2nd theorem is to show that $\varphi\leftrightarrow \mathsf{Con}(\mathsf{PA})$. A variant of the same argument could be applied to $\varphi_n$. 
Let $\mathsf{Con}_n(\mathsf{PA})$ be a natural sentence of the length $\mathcal{O}(\log(n))$ expressing that there are no proofs of contradiction in $\mathsf{PA}$ of the length $\le n$. And let us write $\mathsf{PA}\vdash^m\psi$ to denote that there is $\mathsf{PA}$-proof of $\psi$ of the length $\le m$. The adaptation of mentioned argument from 2nd incompleteness theorem yields
$$\mathsf{PA}\vdash^{P_1(\log(n))} \mathsf{Con}_{P_2(n)}\to \varphi_n\;\;\;\mbox{and}\;\;\;\mathsf{PA}\vdash^{P_3(\log(n))} \varphi_n\to \mathsf{Con}_{\lfloor n^\varepsilon\rfloor},$$
for some polynomials $P_1,P_2,P_3$ and $\varepsilon>0$. 
In fact this two implications are the core of Friedman-Pudlák finite version of 2nd-incompleteness theorem that states that for all strong enough NP-axiomatizable $T$ there is $\varepsilon>0$ such that for all large enough $n$ we have $T\nvdash^{\lfloor n^\varepsilon\rfloor}\mathsf{Con}_n(T)$.
At the same time Pudlák proved that $\mathsf{PA}\vdash^{P(n)} \mathsf{Con}_n(\mathsf{PA})$, for some polynomial $P$. Essentially, this is due to the fact that there are formulas $\mathsf{Tr}_n(x)$ of polynomial in $n$ length that are truth definitions for sentences of the length $\le n$. $\mathsf{PA}$ has a polynomial in $n$ proof that all logical and non-logical axioms of $\mathsf{PA}$ of the length $\le n$ are true according to $\mathsf{Tr}_n(x)$. This allows to prove in $\mathsf{PA}$ by a polynomial in $n$ proof that any $\mathsf{PA}$-proof $p$ consisting of formulas of the length $\le n$ has a conclusion that is true according to $\mathsf{Tr}_n(x)$. And this yield polynomial in $n$ proof of $\mathsf{Con}_n(\mathsf{PA})$. In fact this kind of argument works not only for $\mathsf{PA}$ but for many other natural theories, e.g. $\mathsf{ZF},\mathsf{NGB},\mathsf{EA}$.
Combining the facts $\mathsf{PA}\vdash^{P(n)} \mathsf{Con}_n(\mathsf{PA})$ and $\mathsf{PA}\vdash^{P_1(\log(n))} \mathsf{Con}_{P_2(n)}\to \varphi_n$, we conclude that $\varphi_n$ are provable in $\mathsf{PA}$ by a polynomial in $n$ proof.
[1] Pudlák, P. (1986). On the length of proofs of finitistic consistency statements in first order theories. In Studies in Logic and the Foundations of Mathematics (Vol. 120, pp. 165-196). Elsevier.
