Metamath中的算术，案例研究：Bertrand公设
Arithmetic in Metamath, Case Study: Bertrand's Postulate
摘要：
与其他形式系统不同的是，元数学证明系统没有内置的“十进制数”概念，因为没有预先定义，系统无法识别任意数字串。我们提出了一个系统的定理和定义和算法，应用这些作为基本操作来执行算术计算的步骤数成比例的任意精度的算术计算。我们认为作为案例研究的正式证明贝特朗的假设，这需要计算许多小素数。使用Mathematica实现，我们能够使用大于10的数字完成Metamath中的第一个正式证明。应用的Metamath证明的机械化进行了讨论，并提出了一个启发式的论点，如汤姆黑尔斯的开普勒猜想的证明大型证明的可行性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
