  An arithmetic formula is an expression involving only the constant $1$, and
the binary operations of addition and multiplication, with multiplication by
$1$ not allowed. We obtain an asymptotic formula for the number of arithmetic
formulas evaluating to $n$ as $n$ goes to infinity, solving a conjecture of E.
K. Gnang and D. Zeilberger. We give also an asymptotic formula for the number
of arithmetic formulas evaluating to $n$ and using exactly $k$ multiplications.
Finally we analyze three specific encodings for producing arithmetic formulas.
For almost all integers $n$, we compare the lengths of the arithmetic formulas
for $n$ that each encoding produces with the length of the shortest formula for
$n$ (which we estimate from below). We briefly discuss the time-space tradeoff
offered by each.
