Formalization of the Cauchy Convergence Criterion for Sequences in Coq

The Cauchy Convergence Criterion is a fundamental theory in mathematical analysis. It has a wide range of applications, including sequences, functions, integrals, series, and the completeness of real numbers. Recently, significant progress has been made in the formalization of mathematical theorems, accompanied by strong advocacy for trustworthy mathematics, the strengthening of fundamental mathematical theories has become increasingly important. As a cornerstone of Limit Theory, formalizing the Cauchy Convergence Criterion holds significant importance. This paper utilizes the computer-assisted proof tool Coq, based on the Morse-Kelley (MK) axiomatic set theory formalization system, and employs the real number model provided in Zorich's “Mathematical Analysis” to complete the formal proof of the Cauchy Convergence Criterion for sequences. Through this formal proof, we have established a basis for the formalization of MK-based limit theory and calculus in Coq.