繼“數學機械化叢書”三部專著之后，郁文生教授團隊再推新著：《機器證明:?公理集論及分析基礎的形式化》

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

機器證明 : 公理集論及分析基礎的形式化

郁文生 陳 思 竇國威 郭達凱 冷姝錕 著

北京：科學出版社，2025. 9

ISBN 978-7-03-083244-3

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

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

在我們每本書的結論與注記部分，均對當時 Coq 形式化數學的現狀進行了適當的更新與總結，詳細可見《自然數的緊化延伸機器證明系統》和本書的相應章節，最新進展可參見我們最近發表的綜述論文"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"。本團隊《一元微積分機器證明系統》現已完成，已被科學出版社接受待出版。

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

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

本書合作者都是在讀研究生，在完成本書的多次深入討論中，他們對數學思想的領會，對科學理性、美感的感悟都有了極大的提高，他們為實現書中的證明代碼付出了艱辛的努力，程序完成過程中的個中滋味，體會深刻，相信讀者在理解、運行本書定理機器證明的過程中會有切身的體會。

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

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

在本書正式出版之際，即將迎來四川大學伍炯宇教授和徐安石教授90華誕。作者自1991 年追隨兩位先生攻讀碩士學位，兩位先生深刻的數學思想和嚴謹的科研作風時刻影響著我，終生難忘。謹以此書慶祝伍炯宇先生和徐安石先生90 華誕！祝兩位先生健康長壽！

郁文生 謹識

2025 年4 月

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

ISBN 978-7-03-083244-3

責任編輯: 王麗平 李香葉

本書可作為數學與計算機科學、信息科學相關專業的高年級本科生或研究生教材，也可供從事人工智能相關科研工作者學習參考。

（本文編輯： 劉四旦 ）

專業品質 學術價值

原創好讀 科學品位

一起閱讀科學