布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础。利用交互式定理证明辅助工具Coq,可以完整构建这三大母结构的形式化系统。本文基于计算机证明辅助工具Coq,实现了朴素集合论和点集拓扑学中的拓扑空间的形式化框架。文章内容安排如下:第一章简要介绍了拓扑空间和形式化证明的研究背景和意义。第二章对Coq的基本内容进行了介绍,并给出利用Coq进行定理形式化证明的例子。第三章利用交互式定理证明辅助工具Coq,参考“公理化集合论”体系的构造原理,从集合,映射等数学基础概念出发,实现朴素集合论形式化系统的搭建。朴素集合论的形式化具有高可复用性,可用于构建多种数学系统如序结构,代数结构,微积分等。第四章在朴素集合论的形式化系统上,提出一种选择公理和有标集族直积定理等价性的机器证明。给出选择公理和有标集族笛卡尔积的形式化描述,完成选择公理和有标集族直积定理等价性的证明代码,并在Coq中运行通过。充分体现了基于Coq的数学定理机器证明具有可靠性、规范性、交互性、可读性以及智能性的特点。第五章以上述内容为基础,逐步建立拓扑空间与连续映射,子空间,积空间等相关定义形式化,这对后续研究的有着重要的意义。