(The following is a joke.)

Put and , and define the magic constant $$\xi:=\sum_{n=1}^\infty {n!\over 2^{a_n}}\ =\ 0.630882266676063396815526621896\ldots\quad .$$ Then Try it out!

Factorial does have a closed formula using integer division $\lfloor n/m\rfloor$ due to J. Robinson [1]: we have · $$\begin{align*} · n\bmod m&=n-m\lfloor n/m\rfloor,\\ · \binom rn&=\left\lfloor\frac{(2^r+1)^r}{2^{rn}}\right\rfloor\bmod 2^r,\\ · n!&=\textstyle\left\lfloor2^{n^3}\big/\binom{2^{n^2}}n\right\rfloor=\left\lfloor n^{n^2}\big/\binom{n^n}n\right\rfloor. · \end{align*}$$ · (That is1, $n!=\bigl\lfloor r^n/\binom rn\bigr\rfloor$ for any $r>(2n)^{n+1}$, as the bound is stated in [1]. It actually holds2 already for $r\ge n!\,n^2/2$, which implies3 the second given expression for $n!$.) · In fact, the class of functions $\mathbb N^k\to\mathbb N$ that have a closed expression using $n+m$, $n\mathbin{\dot-}m$$n\cdot m$$\lfloor n/m\rfloor$, and $n^m$ (or even just $2^n$) is quite vast: it coincides with the class of Kalmár elementary functions aka elementary recursive functions. This was proved by Mazzanti [2,§4]. · References · [1] Julia Robinson: Existential definability in arithmetic, Transactions of the American Mathematical Society 72 (1952), no. 3, pp. 437–449, doi 10.2307/1990711. · [2] Stefano Mazzanti: Plain bases for classes of primitive recursive functions, Mathematical Logic Quarterly 48 (2002), no. 1, pp. 93–104, doi 10.1002/1521-3870(200201)48:1%3C93::AID-MALQ93%3E3.0.CO;2-8. · Footnotes · To see that the expression $n!=\bigl\lfloor2^{n^3}/\binom{2^{n^2}}n\bigr\rfloor$ follows from Robinson’s formula, recall that $2^n\ge n+1$ for all integers $n$, thus we have $2^{n-1}=4\cdot2^{n-3}\ge4(n-2)\ge2n$ if $n\ge4$, whence $2^{n^2}>2^{n^2-1}\ge(2n)^{n+1}$; one can check that the expression is valid for $n=0,\dots,3$ by hand. Alternatively, since $n^n\le2^{n^2}$, this expression for $n!$ follows from the other one, proved below. · Since $r^n/\binom rn=n!\prod_{in^2(n-1)$, which implies · $$1-\frac ir=\frac{r-i}r>\frac{2r+i^2}{2r+(i+1)^2}=\frac{1+i^2/(2r)}{1+(i+1)^2/(2r)}$$ · for all $i2r^3+ri^2=r(2r+i^2). · \end{align*}$$ · Thus, · $$\prod_{i