ICMS 2020 Session

Artificial Intelligence and Mathematical Software

Accepted Talk

Yaoshun Fu and Wensheng Yu (Beijing University of Post and Telecommunications)
A formal Proof in Coq of the fundamental theorems of continuous functions on closed intervals
Abstract: Formalized mathematics is getting increasing attention in the mathematics and computing fields. Among them, the formalization of calculus has importance in engineering design and analysis. Therefore, certain properties of functions are particularly essential. In this paper, we present a formal proof of some fundamental theorems of continuous functions on closed intervals based on the Coq proof assistant. In this formalization, we build a real number system referring to Foundations of Analysis of Landau. Then we complete the formalization of the basic definitions of intervals, functions, and limits and formally prove theorems including the completeness theorem, the intermediate value theorem, the uniform continuity theorem and others in Coq. The formalizations embody that mechanical proving of mathematical theorem based on Coq has the characteristics of readability and interactivity. The proof process is normalized, rigorous and reliable. This work gives a foundation for formalizing the theories of topology, analysis, calculus, artificial intelligence, and so on.