郁文生教授團(tuán)隊已在科學(xué)出版社出版了《公理化集合論機(jī)器證明系統(tǒng)》、《分析基礎(chǔ)機(jī)器證明系統(tǒng)》及《自然數(shù)的緊化延伸機(jī)器證明系統(tǒng)》三部專著，被收入“數(shù)學(xué)機(jī)械化叢書”系列，分別為該叢書的第13、14、15 卷，其中兩卷還獲“華羅庚-吳文俊出版基金”部分資助。團(tuán)隊新著《機(jī)器證明: 公理集論及分析基礎(chǔ)的形式化》內(nèi)容與前三部專著雖有重疊，但主要內(nèi)容與作者團(tuán)隊前期完成的工作有很大不同，總結(jié)了作者團(tuán)隊在數(shù)學(xué)形式化研究方面的最新進(jìn)展。

機(jī)器證明 : 公理集論及分析基礎(chǔ)的形式化

郁文生 陳 思 竇國威 郭達(dá)凱 冷姝錕 著

北京：科學(xué)出版社，2025. 9

ISBN 978-7-03-083244-3

《機(jī)器證明 : 公理集論及分析基礎(chǔ)的形式化》利用交互式定理證明工具Coq，實現(xiàn)Morse-Kelley 公理化集合論形式化系統(tǒng)，可以迅速而自然地給出一個數(shù)學(xué)基礎(chǔ)，擺脫了明顯的悖論。在我們開發(fā)的系統(tǒng)中，全部定理無例外地給出Coq 的機(jī)器證明代碼，所有形式化過程已被Coq 驗證，并在計算機(jī)上運行通過，充分體現(xiàn)了基于Coq 的數(shù)學(xué)定理機(jī)器證明具有可讀性、交互性和智能性的特點，其證明過程規(guī)范、嚴(yán)謹(jǐn)、可靠。該系統(tǒng)可方便地應(yīng)用于拓?fù)鋵W(xué)和代數(shù)學(xué)理論的形式化構(gòu)建，實現(xiàn)讀者跟隨計算機(jī)學(xué)習(xí)、理解、構(gòu)建、教育乃至發(fā)展現(xiàn)代數(shù)學(xué)的嘗試，進(jìn)一步提高認(rèn)識數(shù)學(xué)、感受數(shù)學(xué)和欣賞數(shù)學(xué)的素養(yǎng)。為方便應(yīng)用，在Morse-Kelley 公理化集合論形式化系統(tǒng)下，分別給出Landau 的經(jīng)典著作《分析基礎(chǔ)》的形式化系統(tǒng)以及Zorich 的著名著作《數(shù)學(xué)分析》中實數(shù)公理化的形式系統(tǒng)實現(xiàn)，從而迅速且自然地給出數(shù)學(xué)分析的堅實基礎(chǔ)。

本書中公理集論部分的形式化代碼，對作者團(tuán)隊前期《公理化集合論機(jī)器證明系統(tǒng)》中的Coq 代碼進(jìn)行了系統(tǒng)優(yōu)化，代碼量較原先減少了一半以上，刪除了“選擇公理及其等價命題的機(jī)器證明” 一章，增加了“分析基礎(chǔ)的形式化系統(tǒng)實現(xiàn)”以及“實數(shù)公理化的形式系統(tǒng)” 兩章，進(jìn)一步討論了實數(shù)模型的同構(gòu)唯一性及實例化。另外，附錄部分增加了Coq 術(shù)語和指令的說明、本系統(tǒng)定義的策略索引，并給出了公理化集合論和實數(shù)公理化形式系統(tǒng)的結(jié)構(gòu)化表述。本書實現(xiàn)的公理集論和實數(shù)公理系統(tǒng)的形式化系統(tǒng), Coq代碼已較為成熟和完整, 已被Coq官方認(rèn)證, 可以在Coq官網(wǎng)貢獻(xiàn)庫中索引到, 這對僅關(guān)心代碼的讀者提供了便利, 歡迎關(guān)注使用。

在我們每本書的結(jié)論與注記部分，均對當(dāng)時 Coq 形式化數(shù)學(xué)的現(xiàn)狀進(jìn)行了適當(dāng)?shù)母屡c總結(jié)，詳細(xì)可見《自然數(shù)的緊化延伸機(jī)器證明系統(tǒng)》和本書的相應(yīng)章節(jié)，最新進(jìn)展可參見我們最近發(fā)表的綜述論文"A Review on Mechanical Proving and Formalization of Mathematical Theorems" 和 "A Comparative Review of ZFC, NBG, and MK Axiom Systems: Theoretical Foundations and Formalization in Coq"。本團(tuán)隊《一元微積分機(jī)器證明系統(tǒng)》現(xiàn)已完成，已被科學(xué)出版社接受待出版。

自 2022 年以來，隨著CharGPT、Sora、OpenAI 及 DeepSeek、Manus 等大語言模型(LLM)的相繼出現(xiàn)，人工智能學(xué)科的發(fā)展日新月異, 令人眼花繚亂、目不暇接，但測試表明，各類大語言模型對輸出可靠的數(shù)學(xué)證明似乎差強(qiáng)人意，但仍不能令人滿意(這在《自然數(shù)的緊化延伸機(jī)器證明系統(tǒng)》和本書的結(jié)論與注記中已經(jīng)提及)。近年來受菲爾茨獎獲得者 Tao 和 Scholze 用 Lean 形式化數(shù)學(xué)工作的影響，LLM 的出現(xiàn)更是極大地提高了人們對形式化數(shù)學(xué)的認(rèn)識，引起人們的廣泛重視，這一點可通過知網(wǎng)上搜素"Lean+LLM"即可看出。用 LLM 實現(xiàn)各種形式化工具間的轉(zhuǎn)換也是極有意義的研究課題(本書作者團(tuán)隊已初步開展了將 Coq 代碼轉(zhuǎn) Lean 代碼的嘗試研究)。

另外, Coq 官方已經(jīng)確定將 Coq 改名為"The Rocq Prover"(2024 年底已完成)，自 2025 年 2月起, Rocq 官方網(wǎng)站 https://rocq-prover.org 已正式啟用(所有 Coq 代碼依然是有效的)。華裔數(shù)學(xué)家 Terence Tao (陶哲軒) 于 2025 年 5 月開始了對他的《Analysis I》的形式化實現(xiàn) 工 程 ( 見 https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i)。Buzzard 和 Taylor 最 近 也 啟 動 了 對 “ Fermat 大 定 理 ” 的 形 式 化 驗 證 工 程 ( 見https://imperialcollegelondon.github.io/FLT/blueprint.pdf)。在我國，國家自然科學(xué)基金委也專門設(shè)立了有關(guān)“形式化數(shù)學(xué)”的重點項目和揭榜掛帥項目。中國科學(xué)院系統(tǒng)科學(xué)與數(shù)學(xué)研究院也努力爭取將“數(shù)學(xué)形式化與自動推理”列為重要研究方向。

本書合作者都是在讀研究生，在完成本書的多次深入討論中，他們對數(shù)學(xué)思想的領(lǐng)會，對科學(xué)理性、美感的感悟都有了極大的提高，他們?yōu)閷崿F(xiàn)書中的證明代碼付出了艱辛的努力，程序完成過程中的個中滋味，體會深刻，相信讀者在理解、運行本書定理機(jī)器證明的過程中會有切身的體會。

正在本課題組學(xué)習(xí)的一批研究生: 嚴(yán)升、張啟萌、趙佩碩、高暢、劉江昊、王啟明、周艷文、陳寧、陳妍、季婷婷、郁榴苗、張娜、崔洛萍和吉祥等，在提供材料、驗證算例及校對文稿等方面給予了幫助。

最后，感謝國家自然科學(xué)基金(No. 62476028) 對本課題的資助。

在本書正式出版之際，即將迎來四川大學(xué)伍炯宇教授和徐安石教授90華誕。作者自1991 年追隨兩位先生攻讀碩士學(xué)位，兩位先生深刻的數(shù)學(xué)思想和嚴(yán)謹(jǐn)?shù)目蒲凶黠L(fēng)時刻影響著我，終生難忘。謹(jǐn)以此書慶祝伍炯宇先生和徐安石先生90 華誕！祝兩位先生健康長壽！

郁文生 謹(jǐn)識

2025 年4 月

本文摘編自《機(jī)器證明 : 公理集論及分析基礎(chǔ)的形式化》（郁文生等著. 北京：科學(xué)出版社，2025. 9）一書 “前言”“后記”，有刪減修改，標(biāo)題為編者所加。

ISBN 978-7-03-083244-3

責(zé)任編輯: 王麗平 李香葉

本書可作為數(shù)學(xué)與計算機(jī)科學(xué)、信息科學(xué)相關(guān)專業(yè)的高年級本科生或研究生教材，也可供從事人工智能相關(guān)科研工作者學(xué)習(xí)參考。

（本文編輯： 劉四旦 ）

專業(yè)品質(zhì) 學(xué)術(shù)價值

原創(chuàng)好讀 科學(xué)品位

一起閱讀科學(xué)