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.