Largest number definable If $a_n$ is defined as the largest integer definable using $n$ characters in some standard theory like PA or $Z_2$.
Can we prove or disprove that there is some finite integer $k$, such that for all $i>k$, $a_i$ is a perfect power ($m^n$, for $n>1$)? (or very close to one of the form a^b, with $b\gg a$)?
 A: Probably not. Your function $a_n$ is not computable, and is quite sensitive to little details of how we count symbols and exactly what the primitive operations are, which are normally not important enough to be specified with much accuracy in texts.
As for your follow-up question: The function cannot be significantly much smaller than the Busy Beaver function, because we can define the execution of a Turing machine with a PA/Z2 formula that is linear in the size of the machine description. On the other hand, it cannot be significantly much larger than the Busy Beaver, because a for any formula we can specify a Turing machine that searches for a proof that a this formula defines a unique number.
So, apart from some possible horizontal stretching or shrinking, the growth of your formula is equivalent to the Busy Beaver.
A: The sequence $(a_n)$ grows much faster than the Busy Beaver numbers. For example, not only the Busy Beaver sequence $BB(n)$ but also expressions like $BB(BB(n))$ and $\underbrace{BB(\cdots(BB(}_{n\text{ times}}n)))$ are definable in PA with formulas of length not much longer than the length of the smallest formula defining $n$ (in particular, with length sublinear in $n$). This is because the functions $n\mapsto BB(n)$, etc are definable in PA, so to define a value of the function at a specific integer you just have to combine the definition of the function (which has constant length) with the definition of the integer.
By the way, there are two reasons that Henning Makholm's suggested Turing machine wouldn't work: first of all, it might not find a proof that the formula in question defines an integer (since although the fact that the formula defines an integer is true, it may not be provable), and secondly, even if it did find a proof that the formula defined an integer, it would have no way of converting that proof into information about what the value of that integer is.
