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

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

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

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

ISBN 978-7-03-083244-3

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

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

在我們每本書的結(jié)論與注記部分，均對當時 Coq 形式化數(shù)學的現(xiàn)狀進行了適當?shù)母屡c總結(jié)，詳細可見《自然數(shù)的緊化延伸機器證明系統(tǒng)》和本書的相應(yīng)章節(jié)，最新進展可參見我們最近發(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"。本團隊《一元微積分機器證明系統(tǒng)》現(xiàn)已完成，已被科學出版社接受待出版。

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

另外, Coq 官方已經(jīng)確定將 Coq 改名為"The Rocq Prover"(2024 年底已完成)，自 2025 年 2月起, Rocq 官方網(wǎng)站 https://rocq-prover.org 已正式啟用(所有 Coq 代碼依然是有效的)。華裔數(shù)學家 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)。在我國，國家自然科學基金委也專門設(shè)立了有關(guān)“形式化數(shù)學”的重點項目和揭榜掛帥項目。中國科學院系統(tǒng)科學與數(shù)學研究院也努力爭取將“數(shù)學形式化與自動推理”列為重要研究方向。

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

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

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

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

郁文生 謹識

2025 年4 月

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

ISBN 978-7-03-083244-3

責任編輯: 王麗平 李香葉

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

（本文編輯： 劉四旦 ）

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

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

一起閱讀科學