Formalization of General Topology in Coq — A Formal Proof of Tychonoff's Theorem

The order, algebra and topology of the Bourbaki group are the foundation of modern mathematics. On the basis of the proof assistant Coq, the formal system of these three major parental structures can be constructed completely. On the basis of the formalization of axiomatic set theory, this paper present the formal framework of general topology. This paper completes the formalization of some basic definitions of general topology, including base, subbase, topology, and compact space. In addition, the formal proof of the Alexander subbase theorem is proposed on the basis of Tukey’s lemma. Finally we complete the formal proof of Tychonoff’s theorem, which is famous in general topology. All formal processes have been verified in Coq, which demonstrates the reliability, readability and rigor.