Let $f(n)$ be the length of the shortest statement whose shortest proof has length $n$ or more.
What are the asymptotics of $f(n)$? With standard symbols and length counted by character.
For any standard theory, such as PA or ZFC.
Let $f(n)$ be the length of the shortest statement whose shortest proof has length $n$ or more.
What are the asymptotics of $f(n)$? With standard symbols and length counted by character.
For any standard theory, such as PA or ZFC.
In any theory to which Gödel's theorems apply, this is going to grow extremely slowly, in the following very strong sense. Suppose $g(m)$ is a function such that for any positive integer $m$, $f(g(m)) > m$. Then given a statement $S$ of length $\le m$, if $S$ is provable the shortest proof of $S$ must have length at most $g(m)$. But then $g(m)$ can't be a computable function (otherwise we could test whether $S$ is provable by enumerating all proofs of length at most $g(m)$, and we'd have an algorithm for solving the Halting Problem).
Putting it another way, for any computable function $g: {\mathbb N} \to {\mathbb N}$, there is some $m$ such that $f(g(m)) \le m$.