2015/03/09 by Mario Carneiro, Carneiro, Mario
Computer Science · Mathematics · #03F03 #11A51 (Secondary) #65Y04 (Primary) 03B35 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #G.1.0 #Logic (math.LO) #Logic in Computer Science (cs.LO) #acm:03B35 #acm:03F03 #acm:11A51 #acm:65Y04 #cs.LO #math.LO #msc:03B35 #msc:03F03 #msc:11A51 #msc:65Y04
paper · pdf · doi:10.48550/arxiv.1503.02349
16 pages, 0 figures; submitted to CICM 2015
arxiv created 2015/05/03 · arxiv updated 2015/05/05
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.