%0 Journal Article
%A SUN Tian-yu
%A YU Wen-sheng
%T A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma
%D 2019
%R 10.13190/j.jbupt.2019-001
%J Journal of Beijing University of Posts and Telecommunications
%P 1-7
%V 42
%N 5
%X On the basis of the computer proof assistant Coq, a formal proof of the equivalence between the axiom of choice and Tukey's lemma is presented. The formal description of axiom of choice and Tukey lemma was given based on the "axiomatic set theory" formal system, which was the first formalization of Tukey's lemma. A complete proof code of the equivalence between the axiom of choice and Tukey's lemma was completed. All the proofs were formally checked in Coq. The formal proof demonstrated that the Coq-based mechanized proof of mathematics theorem had the characteristics of readability and interactivity. The proof process was standardized, rigorous and reliable. This formal work has important applications in many fields of formal mathematics, especially in set theory, topology and algebra.
%U https://journal.bupt.edu.cn/EN/10.13190/j.jbupt.2019-001