ICMS 2020 Session

Artificial Intelligence and Mathematical Software

Accepted Talk

Tianyu Sun and Wensheng Yu (Beijing University of Post and Telecommunications)
Formalization of the Axiom of Choice and its Equivalent Theorems in Coq
Abstract: Formal verification technology has been widely applied in the fields of mathematics and computer science. The formal proof of famous mathematical theorems is particularly essential. In this paper, we describe the formalization of the axiom of choice and several of its famous equivalent theorems in the Morse-Kelley set theory. These theorems include Tukey's lemma, the Hausdorff maximal principle, the maximal principle, Zermelo's postulate, Zorn's lemma, and the well-ordering theorem. We prove the above theorems by the axiom of choice in turn, and finally prove the axiom of choice by Zermelo's postulate and the well-ordering theorem, thus completing the cyclic proof of the equivalence between them. The proofs are checked formally using the Coq proof assistant in which Morse-Kelley set theory is formalized. The whole process of formal proof demonstrates that the Coq-based formal proof of mathematics theorem is highly reliable and rigorous. The formal work of this paper is enough for most applications, especially in set theory, topology, and algebra. It will become an essential theoretical basis for mathematics and computer science.