Arithmetic in Metamath, Case Study: Bertrand's Postulate

Mario Carneiro

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 w…