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