布爾巴基學(xué)派的序、代數(shù)、拓撲三大母結(jié)構(gòu)是現(xiàn)代數(shù)學(xué)的基礎(chǔ).利用計算機證明輔助工具,可以完整構(gòu)建這三大母結(jié)構(gòu)的形式化系統(tǒng).《公理化集合論機器證明系統(tǒng)》利用交互式定理證明工具Coq,實現(xiàn)Morse-Kelley公理化集合論形式化系統(tǒng),包括對該體系中8個公理(含選擇公理)和1個公理圖示以及全部181條定義或定理的Coq描述,其中構(gòu)造了序數(shù)和基數(shù),定義了非負整數(shù),把Peano公設(shè)當作定理,可以迅速而自然地給出一個數(shù)學(xué)基礎(chǔ),擺脫了明顯的悖論.這是Morse-Kelley公理化集合論系統(tǒng)的首次形式化實現(xiàn).在Morse-Kelley公理化集合論形式化系統(tǒng)下,作為應(yīng)用,我們給出選擇公理與它的幾個著名等價命題間等價性的機器證明,這些命題包括Tukey引理、Hausdorff極大原則、極大原則、Zorn引理、良序定理及Zermelo假定等.在我們開發(fā)的系統(tǒng)中,全部定理無例外地給出Coq的機器證明代碼,所有形式化過程已被Coq驗證,并在計算機上運行通過,體現(xiàn)了基于Coq的數(shù)學(xué)定理機器證明具有可讀性和交互性的特點,其證明過程規(guī)范、嚴謹、可靠.該系統(tǒng)可方便地應(yīng)用于拓撲學(xué)和代數(shù)學(xué)理論的形式化構(gòu)建.