基于Coq的两个重要极限的形式化证明

Mathematics mechanization is mainly to use computers to realize the reasoning of mathematical theorems, and formal mathematics is an important content of mathematical mechanization. This paper uses the interactive theorem proving tool Coq to realize the formal proof of two important limits.It mainly includes the definition of concepts such as set, sequence, function, limit and the proof of related theorems. On this basis, the related theoretical system of series was established, and the theorems such as Cauchy criterion, convergence method of positive series, and the nature of absolute convergence were formally proved. The formal definition of the sine function is given through the series, and the formal proof of two important limits is realized. All codes involved in this article have been verified in Coq, which fully reflects the high credibility of Coq.