郁文生，窦国威：自然数的紧化延伸机器证明系统

数系的扩充始终贯穿于数学理论的发展之中。

数学史上最令人惊奇的事实之一，是实数系的逻辑基础竟迟至19 世纪后叶才建立起来。自然数理论公理体系的建立更是基于Dedekind 总结出的五条基本性质、以Peano 发表于1889 年《算术原理——用一种新方法展现》为标志。历史上，对实数完备性的深刻认识体现在分析算术化的过程之中，而分析算术化的过程与克服数学史上著名的三次危机，即无理数的发现、分析的严密化、集合论中悖论的消解是密切相关的。

另一方面，历史不断会出现惊人相似的一幕。对于非标准实数本质的认识，是人们20 世纪现代数学时期对数系研究的最新成果。

在Robinson 的名著Non-Standard Analysis 的序言中曾引用Gödel 的话:

“算术从整数开始进而通过有理数、负数、无理数等等把数系扩大。但是，在实数之后，下一个十分自然的步骤，即引入无限小，竟被完全忽略了。我认为，在未来的世纪里，人们会把这看作数学史上的一件大怪事，就是在发明了微积分三百年之后，第一个精确的无限小理论才发展起来。”

在实数中引入“理想元素” 的实无穷小恰是三百年前Leibniz 在发明微积分时的最初设想，但因当时违背传统、暂不合逻辑而未被接受。古典分析建立在否认无限小存在的数域上。非标准分析则是在确立了包含无限小元素的某种数域的前提下进行严谨论述的。非标准分析成功地解决了三百年前涉及无限小的古老悖论，也使古希腊人想用分数表示实数的思想得以实现。对于无限——实无限，数学从最初的回避（初等数学时期）到被迫面对（古典分析时期），直到如今的积极主动研究（现代数学时期），经历了漫长而艰辛的探索思考过程。Gödel认为: “我们有充分的理由相信，以这种或那种形式表示的非标准分析，将成为未来的分析学。” 我国著名数学家吴文俊院士也曾说: “非标准分析才是真正的标准分析。”

从数系的扩充角度来看非标准分析，其要害是承认实无穷小和实无穷大，其基础理论是超实数理论。超实数域是实数域的一个扩张，它包括了实无穷小和实无穷大。绝大多数涉及超实数理论的非标准分析文献，都是用超幂方法给出超实数域的一个模型。这种扩充是在承认已建立有标准的实数模型的基础上进行的。

中国科学技术大学汪芳庭教授在其《数学基础》中独辟蹊径，以算术超滤模型代替超幂模型，采用算术超滤分数构造实数，使方法更为直接、简洁，让“无穷大自然数” 以算术超滤身份直接进入了数学，而且这一构造方法与古典分析中从整数到有理数的扩充方法达到了完全统一！

关于对“滤子” 和“超滤” 等基本概念，汪芳庭教授在其专著《算术超滤——自然数的紧化延伸》的前言中有几段形象的说明，有助于读者对这些概念进行深入理解，内容如下:

“自然数集上的一个滤子（filter），就是自然数性质（关系）的一种相容组合。其实，使用‘滤子’ 一词，不如使用‘关系网’ 一词更加妥帖。超滤，实际上是‘极大关系网’。一个主超滤，就是一个自然数所具有的一切性质（关系）的总和。‘非主超滤’即无具体自然数与之对应的‘极大关系网’。 “有句名言: ‘人的本质……是一切社会关系的总和。’ （马克思: 《关于费尔巴哈的提纲》，1845 年）在有此话的半个多世纪后，随着集合论诞生，超滤（极大关系网）的概念出现了。20 世纪30 年代，人们对自然数本质的这种认识方式与之前对人的本质的一种认识方式达到了相同的哲学高度。 “超滤空间是离散自然数空间的一种紧化。”

近年来，随着计算机科学的迅猛发展，特别是证明辅助工具Coq 的出现，数学定理的计算机形式化证明取得了长足的进展。Coq 的基本原理是归纳构造演算，是一个交互式定理证明与程序开发系统，可用于描述定理内容、验证定理证明。Coq 的交互式编译环境，使用户以人机对话的方式一问一答，可以边设计、边修改，使证明中的疏漏及时得到补证。进入21 世纪，随着“四色定理”、“有限单群分类定理” 及“Kepler 猜想” 等一系列著名数学难题形式化证明的实现，各种计算机证明辅助工具在学术界得到了广泛认可。

1998 年菲尔兹奖获得者Gowers、2002 年菲尔兹奖获得者Voevodsky、2006年菲尔兹奖获得者Tao、2010 年菲尔兹奖获得者Villani 和2018 年菲尔兹奖获得者Scholze 都大力倡导发展可信数学。1987 年沃尔夫奖和2005 年阿贝尔奖获得者Lax 认为“（高速计算机）对于应用数学和纯粹数学的影响可以与望远镜对天文学和显微镜对生物学的影响相比拟”。著名数学家和计算机专家Wiedijk 甚至认为当前正在进行的形式化数学是一次数学革命。

应当指出，在数学定理机器证明方面，1960 年，美籍华裔著名数理逻辑学家王浩基于名为“自然演绎” 的逻辑系统编写了一个程序，仅用几分钟时间就机器证明了Whitehead 和Russell 著名的Principia Mathematica 中的350 多个纯谓词演算定理，并提出应将诸如Landau 的数系、Hardy-Wright 的数论、Hardy 的微积分、Veblen-Young 的射影几何、Bourbaki 出版的书卷等数学教材作为纲领，机器验证所有证明并保证细节的严谨性。20 世纪70 年代，由中国数学家吴文俊院士开创的“吴方法” 的研究在国际上是独具特色和领先的。吴文俊院士早年留学法国，深受布尔巴基学派的影响，在拓扑学领域取得了举世瞩目的成果，晚年致力于数学定理机器证明的研究，并提出了数学机械化纲领。吴先生开创的定理机器证明“吴方法” 主要基于多项式代数方法，依赖符号计算和数值计算，有完备的算法，但算法复杂性高，在变量或参数过多的情况下，受硬件物理条件限制。形式化证明主要基于逻辑的推理，通过人机交互，可将人的智慧和机器的智能结合起来。将计算机辅助证明工具Coq 和基于符号数值混合计算的多项式代数方法结合，是非常有吸引力的研究课题。实现拓扑学的机器证明也是吴文俊院士的一个夙愿。

← 左右滑动查看详细信息→

《自然数的紧化延伸机器证明系统》（郁文生，窦国威著. 北京：科学出版社，2024. 5）的主要贡献是: 利用交互式定理证明工具Coq，在Morse-Kelley 公理化集合论形式化系统下，给出汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证。在我们开发的系统中，全部定理无例外地给出Coq 的机器证明代码，所有形式化过程已被Coq 验证，并在计算机上运行通过，充分体现基于Coq 的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。

本书可供集合拓扑、数论、数理逻辑、数学基础、数学教育与数学哲学及计算机科学、信息科学相关专业的高年级本科生、研究生、教学与研究人员学习参考，也可供从事人工智能相关科研工作者参考。

国家自然科学基金委对本课题（No. 61936008）给予资助。

本文摘编自《自然数的紧化延伸机器证明系统》（郁文生，窦国威著. 北京：科学出版社，2024. 5）一书“前言”，有删减修改，标题为编者所加。

（数学机械化丛书）

ISBN 978-7-03-077545-0

责任编辑: 王丽平 李香叶

本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教学用书，也可供从事人工智能相关科研工作者学习参考。

（本文编辑：刘四旦）

一起阅读科学!

科学出版社│微信ID：sciencepress-cspm

专业品质 学术价值

原创好读 科学品位

科学出版社视频号

硬核有料 视听科学