  Unlike some other formal systems, the proof system Metamath has no built-in
concept of "decimal number" in the sense that arbitrary digit strings are not
recognized by the system without prior definition. We present a system of
theorems and definitions and an algorithm to apply these as basic operations to
perform arithmetic calculations with a number of steps proportional to an
arbitrary-precision arithmetic calculation. We consider as case study the
formal proof of Bertrand's postulate, which required the calculation of many
small primes. Using a Mathematica implementation, we were able to complete the
first formal proof in Metamath using numbers larger than 10. Applications to
the mechanization of Metamath proofs are discussed, and a heuristic argument
for the feasability of large proofs such as Tom Hales' proof of the Kepler
conjecture is presented.
