nonasymptotic complexity results

The general fact surrounding some of the other answers is
the following:

Every computably axiomatizable consistent theory $T$
containing trivial arithmetic admits very short theorems
requiring extremely long proofs.

The basic fact is that there can be no total computable
bound on the length of the proof required. To see this,
suppose that there is a computable total function $f$ such
that whenever statement $psi$ is a statement of size at
most $n$ provable from $T$, then there is a proof of size
at most $f(n)$. In this case, the question of whether $T$
proves $psi$ will be decidable, since we can simply
inspect all proofs of length $f(n)$, where $n=|psi|$ and
check if any of them are proofs of $psi$. But it is
impossible that $T$ proves $psi$ is decidable, since we
could then produce a consistent completion of $T$, by the
usual process of completing a theory, which is effective
for decidable theories. This would produce a computable
complete consistent theory of arithmetic, in contradiction
to the incompleteness theorem.

One can make the conclusion fairly concrete via the halting
problem. If $T$ is true and contains some trivial
arithmetic, then $T$ will prove all true instances of the
assertion program $p$ halts on input $m$, and prove no
false instances. If there were a total computable function
$f(p,m)$ such that whenever $p$ halted on input $m$, then
there was a proof of this of length at most $f(p,m)$, then
we could decide the halting problem: on input $(p,m)$,
compute $f(p,m)$ and then look at all proofs of that length
and determine if there is a proof of halting or not.

In conclusion:

Theorem. For any computably axiomatizable true theory $T$ and for any total computable
function $f$, there is a program $p$ and input $m$ such
that $T$ proves that $p$ halts on input $m$, but there is
no proof of this in fewer than $f(p,m)$ steps.

Since as we all know, the computable functions can grow
quite outrageously, this means that for any theory there
will be short theorems that require extremely long proofs.