Explicit formula for $a_0=1$, $a_{n+1}=a_n^2+1$

Question

Is there an explicit formula in elementary function for the sequence $a_n$ where $a_0=1$, $a_{n+1}=a_n^2+1$? How does one prove or disprove such claims?

Edit: I think my question may be formulated in the following way: Is there an elementary function $f$ which satisfies $f(0)=1$ and $f(n+1)=f(n)^2+1$?

Answer 1

According to A. V. Aho and N. J. A. Sloane, Some doubly exponential sequences, Fib. Quart., 11 (1973), 429-437, $$ a(n+1) = \text{round}(b^{2^n})$$ where $b$ is a certain real number, approximately $2.25851845058946539883779624006373187243427469718511465966\ldots$

Answer 2

As the sequence is very quickly growing, past a certain term, let $a_m$, the $+1$ becomes really tiny and the iterates are well approximated by

$$x_n=(x^m)^{2^{n-m}}.$$

An interesting question is if it holds that

$$x_n\sim c^{2^n}$$ where $c$ would be

$$\lim_{n\to\infty}\sqrt[2^n]x_n.$$