Machine proving system for mathematical theorems in Coq — Machine proving of Hausdorff maximal principle and Zermelo postulate
Tianyu Sun, Wensheng Yu · 2017
Under the axiomatic set theory frame, this paper implements the machine proving of the equivalence between the Axiom of Choice and several of its famous equivalent theorems using Coq as an interactive theorem proving tool. These theorems include Tukey lemma, Hausdorff maximal principle, Maximal principle and Zermelo postulate. The proving process demonstrates that the Coq-based machine proving of mathematics theorem is highly readable, interactive, rigorous and reliable.