数学机械化思想的产生和发展

◎ 傅海伦

（山东师范大学数学科学学院）

数学机械化的思想已经启示人们以更为开阔的视野去审视数学的现状，从新的角度来思考和勾画数学发展的前景。数学机械化的思想从产生到发展曾吸引无数数学大师以及数学家们为之倾注心血，他们坚持不懈地探索和研究，表明了数学机械化思想重要而深刻。然而，数学机械化的道路毕竟是漫长而艰难的。探索数学机械化思想产生和发展的道路，追寻这些数学大师以及数学家们的足迹，将有利于促进数学机械化问题的研讨和发展，开创新局面。

一、对机械化、数学机械化及其特征的理解和认识

何谓机械化？按我国当代著名数学家吴文俊先生的理解，“所谓机械化，无非是刻板化和规格化”。[1]吴先生借用现代机器和计算机的工作来说明“机械化”：一方面，无论是机器代替体力劳动，或是计算机代替某种脑力劳动，其所以成为可能，关键在于所需代替的劳动已经“机械化”，也就是说已经实现了刻板化和规格化；另一方面，随着现代机器性能和计算机技术的提高，大量复杂的劳动可交由机器操作进行，这必然会进一步刺激并促进脑力劳动的机械化。简单刻板的机械化动作，不仅可以让机器来实现，还为自动化铺平道路，就这一意义来说，数学中的某些脑力劳动与体力劳动颇有共同之处，它们也就同样可以机械化[2]。数学由于符号形式而易于运算和推理，故研究问题时，人们可以暂时撇开符号的意义而仅着眼于形式，当符号与一定的概念单值对应时，思想的操作可转换为对符号的操作，而符号的操作可委托机器进行，故人们利用符号借助于计算机，便可使复杂、繁重的脑力劳动机械化，从而实现智力的解放。从认识论上分析，数学思维既有创造性活动又有非创造性活动，二者又是互为前提、相互制约、相互转化的。非创造性工作是创造性工作的基础，创造性工作又可以通过某种途径部分地转化为非创造性工作。当我们通过构造算法程序把求解问题的创造性工作转化为非创造性工作之后，也就有可能把问题的求解过程交由机器来完成，这便是数学思维活动的机械化。数学问题的机械化就要求在运算或证明过程中，每前进一步之后，都要有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。

由此看来，所谓数学机械化，即是把要求解或证明的某一类问题（这类问题可能成千上万，也可能无穷无尽）当作一个整体加以考虑，以建立一种统一的、确定的计算或证明程序，使得该类中的每一个问题，只要按照此程序机械地（刻板地）、按部就班地一步一步实施下去，经过有限步骤之后即可求解问题的解或推断出数学命题的结论是否为真，命题为真时即为定理。对一类问题而言，这种统一的、确定的求解或证明的方法称为数学问题的机械化方法，一般表现为机械化程序。它具有以下几个特点：

（1）确定性。即程序是“一义”的规定，没有歧义的理解，程序运作完全是可行的。

（2）预见性。在执行这个程序时，每一步都可预见到下一步该怎么办。

（3）普适性。即程序适用于解决问题所在的同一类的其他任何一个问题。

（4）具体性。即实现具体求解，能在有限步骤内达到“最后”一步，即出具体结果。

数学机械化又是创造性思维和非创造性思维活动的统一。建立统一的、确定的计算或证明的机械化程序的过程就是创造性思维活动的过程，这是实现数学机械化的关键，而按照固有的程序实施机械化求解或证明的操作，这是将思维的创造性工作部分地转化为非创造性工作的过程，也是完成思维的机械化结果的过程。

二、数学机械化思想来源于中国古算，中国古代数学乃是机械化体系的代表

数学机械化思想来源于中国古算，并贯穿于中国古算整个发展过程之中。与古希腊及其延续的数学公理化和演绎推理的传统相对应，中国古算以算法为中心，注重计算和计算技术的提高，以解决问题为主旨，几乎不考虑离开数量关系的图形的性质，而是通过切实可行的方法把实际问题化归为一类数学模型，然后构造一套机械化的算法，并按照程序化的要求，一步步求出具体的数值解，算法的程序化是中国古代数学的重要特点，算经中的“术”全是计算公式或计算程序或应用这些公式、程序的细草。所有的问题都要算出具体数值作为答案，即使是与图形有关的几何问题也不例外。这就是几何方法与算法的有机结合，或几何问题的算法化。这种从实际问题出发，建立算法的机械化一直是古代中国数学研究的传统，也是中国算家所努力的方向乃至孜孜以求的目标。成书于公元前一世纪的《九章算术》是中国算法机械化的光辉典范。书中归纳了九类数学问题，每章中讨论一类，以术文统率应用问题的形式，给出解答和求解方法。从问题出发“寓理于算、不证自明”是该书的特点。书中提出了世界上最早最完整的分数四则运算法则及各种比例和比例分配算法，也提出了世界上最早、最完整的多位数开平方、开立方程序，线性联立方程组的解法程序及有关正负数的概念及移项法则，也最早见于此书，其中解线性方程组的机械消法要比高斯（Gauss）早1800多年。

《九章算术》中的机械化思想被后代中算所继承和不断发展，魏晋时数学泰斗刘徽发展了多种算法，其《九章算术》注是对数学机械化算法的重大贡献。刘徽以率的概念及基本运算为“纲纪”，实现了筹式运算的模式化和程序化，从而把以筹算为基础的算法提高到理论的高度。开平方、开立方的机械化程序，到宋代更发展成为高次代数方程求数值解的统一的机械化算法。十一世纪数学家贾宪的求贾宪三角各廉的增乘开方法，由贾宪开创而秦九韶完善的求高次方程正根的正负开方术，《数书九章》中的大衍求一术解法，李冶的天元术等都是一套套比较复杂的计算程序，许多程序可以直接搬到现代电子计算机上去实现。被西方推崇为中世纪最伟大的数学家朱世杰[3]，其数学名著《四元玉鉴》（公元1303年）中，已给出了高次代数联立方程组的解法（未知数的个数最多可达4个）。“吴文俊解释并发展朱世杰《四元玉鉴》中的解高次联立代数方程组的有效算法，成为机械化证明的代数基础。”[4]不仅如此，宋元时期的“天元术”引进了天元，并为发展天元术而建立了一整套的代数机器，包括天元、地元、人元、物元等相当于现代未知数的概念，并建立这些元正负乘幂及其代数式运算系统，即可把几何问题转化为代数方程或方程组的求解问题。所有这些，正是所谓笛卡儿（Descartes）的最主要的贡献所在，是解析几何得以创立的决定性一步[5]。第二次世界大战之后，电子计算机的诞生、普及和发展，促使人们重新认识以中国为主体的古代东方数学的程序化思想与机械化算法体系。实际上，中国古代数学的许多计算方法程序不仅是和现代计算机原理相通的，而且这些思想对今天的数学发展和教学研究仍有重要的启迪作用。吴文俊关于数学机械化的研究工作，就是这些思想和成就启发下的产物，它是我国自《九章算术》以迄宋元时期数学的直接继承。[6]

三、数学机械化思想的产生和发展

数学机械化思想来源于中国古算，在数学发展史上，不仅中国古代的众多数学家和数学大师为之作出了重大贡献，而且吸引了无数西方数学家为之倾注心血。数学机械化就沿着这些数学家及数学大师们坚持不懈地求索所开辟的道路向前一步步发展。

1．有关笛卡儿（Desartes）宏伟的设想

17世纪中叶，建立坐标系从而把变量引入数学的法国数学家、哲学家、机械哲学的奠基人——笛卡儿，在其未发表的著作中提出过宏伟的设想：一切数学问题都可化为代数问题，而一切代数问题都归结为单个代数方程的求解问题。即可表为：

这里Pi（i=1，2，…，n）及P均为多项式。

尽管笛卡儿的设想未能实现，但这一深刻的思想对其后的数学发展有着重大的影响。现在知道，上述每一步未必行得通，即使行得通是否现实可行也是问题。我国的著名数学家吴文俊先生曾在此方面作出了贡献。首先他认真研究了笛卡儿的宏伟计划及其与中国传统数学的关系，指出：“回顾我国从秦汉到宋元间数学发展的历程，可谓我国传统数学所走过的道路正好与笛卡儿的计划若合一契；反过来笛卡儿的计划，也无异于为中国传统数学作了一个很好的总结”。[7]在此基础上，他提出一套完整的算法，使得代数方程组通过机械步骤消元变成一个代数方程，并将解代数方程组扩大为带微分的代数方程组，从而大大扩张研究问题的范围，这种方法不仅能证明定理，而且能自动发现定理，这大大优越于现有的任何方法[8]。

2．莱布尼兹（Leibniz）的初步尝试

微积分学的先驱莱布尼兹第一个明确提出应用数学方法来研究逻辑的思想。为此他提出“彻底的符号化”并发展起相应的推理演算，这是指将推理的有效性问题转化为计算的正确性问题，这实质上包含了应使推理演算化的思想：由于实现了彻底的符号化，因此，在所谓的“通用语言”（通过使用简单明了的符号及合理法则，已不再具有自然语言所固有的诸如含糊性、不规则性弊病，从而也就将取代自然语言而成为理想的、世界性的公共语言）中，逻辑推理的过程就相当于符号（系列）的变形，而这在通常数学中所作的计算如（a+b）2=a2+2ab+b2等等，是十分相似的，也即是一种演算过程。为了实现这一使逻辑“数学化”的计划，莱布尼兹设相过数学领域的推理机器，这可看作机械化思想的初步尝试。他已清楚地认识到这一计划的重要性，曾预言：“一旦完成了这一计划，人类就将获得这样一种新工具，它对于人类理解能力的增强程度将永远超出任何一种光学仪器对于视力的加强”[9]。但是，莱布尼兹并没有能实际地去实现自己的计划。

3．希尔伯特（Hiblert）机械化定理的提出

对20世纪数学发展曾作出重大贡献的希尔伯特最先从理论上明确提出定理证明机械化的思想。他在1899年出版的经典名著《几何基础》（Grundlagen der Geometrie）中叙述了数学机械化的思想，并写进了数学著作中最早出现的一条机械化定理：[10]初等几何中只涉及从属与平行关系的定理证明可以机械化。这就是著名的希尔伯特机械化定理，希尔伯特这一名著是以公理化的典范而著称于世的，但吴文俊认为，该书更重要之处，是在于提供了一条从公理化出发，通过代数化以达到机械化的道路[11]。事实上，希尔伯特本人在其数十年的数学生涯中，一直遵循一条几何代数化的道路来不断探求数学机械化途径：从公理系统出发，建立坐标系，引进数系统，把几何定理的证明转化为代数式的计算，这正是一条从公理化走向代数化直至数值化的道路。然而，希尔伯特对数学这一深刻的认识却长期为数学家们所忽视。

4．定理的机器证明

近代的机器证明思想由莱布尼兹首先提出，并直接导源于他的定理证明机械化设想。到19世纪末，希尔伯特等创立并发展了数理逻辑，为定理证明机械化提供了一个强有力的工具，使这一设想有了明确的数学形式，又由于20世纪40年代电子计算机的出现，才使这一设想的实现有了现实可能性。到50年代，机器证明开始兴起成为一个数学领域。所谓定理的机器证明，是指使用计算机证明定理的成立，即把人证明定理的过程，通过一套符号体系加以形式化，变成一系列在计算机上自动实现的符号计算过程。其实质是把具有智能特点的推理演绎过程机械化。定理的机器证明是人工智能的主要研究课题之一。“从传统的手工证明到定理的机器证明，是现代数学思想方法的一次重大突破”。[12]

机器证明史上第一次奠基性的突破，是由美国的卡尔基大学—兰德公司协作作出的。1956年，此协作组的纽厄尔（A.Newell）、西蒙（H.Simon）和肖乌等人通过研究证明定理的心理过程，建立了机器证明的启发或搜索法，编制了一个“逻辑理论机”程序（LT），成功证明了罗素和怀特海所著的《数学原理》第二章52条定理中的38条，这一年可作为历史上计算机证明以至于人工智能研究的开端。1963年，他们又在计算机上证明了全部52条定理。50年代末，著名美籍华人王浩教授发明了王浩算法，把机器证明规则化。1959年，他只用9分钟的机器时间，用计算机证明了《数学原理》中的一阶逻辑部分的全部350多条定理，在当时数学与数理逻辑界引起轰动。[13]70年代，机器证明得到新的重大进展，1976年美国的阿佩尔（K.Appel）、哈肯（W.Haken）等人在电子计算机上解决了一百多年来传统人脑支配手工操作所长期未能解决的著名难题——“四色猜想”问题。此外，机器证明在分析拓扑学、集合论以至递归函数等方面都使机器证明获得了成功的应用。[14]

我国的数学家在机器证明研究上取得了显著成果，引起了国内外学术界的关注。吴文俊在对中国古算深入研究的基础上，分析了笛卡儿的思想，深入探讨希尔伯特《几何基础》一书中隐藏的构造性思想，开拓机械化数学的崭新领域。他提供了平面几何及微分几何的判定法，在机器上证明了人难以证明的问题[15]。1976年冬开始研究，1977年春取得初步成果。证明了初等几何主要一类定理的证明可以机械化。其证明方法分为三个主要步骤：

第一步，从几何的公理系统出发，引进数系统与坐标系统，使任意几何定理的证明问题成为纯代数问题。

第二步，将几何定理假设部分的代数关系式进行整理，然后依确定步骤验证定理终结部分的代数关系式是否可以从假设部分已整理成序的代数关系式中推出。

第三步，依据第二步中的确定步骤编成程序，并在计算机上实施，以得出定理是否成立的最后结论。[16]

实际上，吴文俊给出了实现机器证明的一个行之有效的一般方法，其方法称为“吴文俊消法”或“吴方法”，可以说，这是以中国传统数学的构造性和机械化思想方法应用的结果。首先遵循机械化思想引进数系、建立坐标系，把几何构图中的各种关系利用代数方程来描述。将数学定理的假设条件表示为一组代数方程

而数学定理的结论由代数方程

C：g（x1，x2，…，xn）=0

所刻画，这里f1，f2，…fr和g都是变化x1，x2，…，xn的多项式，那么定理的机械化证明就可归结为如下的机械化问题：构造并提供一种确定的、机械的算法，使得依此算法进行有限步之后即可判定：在若干附加条件下，结论C是否可由假设H推出，即是否可由f1=0，f2=0，…，fr=0推出g=0。

数学定理机械化证明的吴氏定理完满地解答了这一机械化问题[7]。吴文俊继承和发展朱世杰《四元玉鉴》解高次联立代数方程组的有效解法，成为机械化证明的代数基础，吴原理提供了高次联立方程组求解的有效方法[18]。该法就解多元多项式组的方程组而言，是当今世界上唯一能包括一般情形的完整算法。自1976年以来，周咸青[19]用“吴方法”已成功地证明了600多条定理，以吴氏定理为基础，机器证明定理的范围又被推广到非欧几何、仿射几何、圆几何、线几何、球几何等等领域，1978年，又证明初等微分几何中的一些主要定理可以机械化，这样走出完全是中国人自己开拓的新数学道路。到80年代，吴文俊不仅建立起数学机械化证明的基础，而且扩张成广泛的数学机械化纲领。吴法已在数理科学、系统科学、理论物理和计算机科学等基础科学领域获得了成功的应用，解决了一系列理论和实际问题。

近年来，对于中国数学史的研究及从定理机器证明的数学机械化纲领正在急剧地扩大影响，真正成为一个独具中国特色的结构性的、可机械化的数学运动。1990年8月8日，以吴文俊为首的“数学机械化中心”正式成立。在吴文俊的总纲领下，他的同事及学生吴文达、石赫、刘卓军、王东明、胡森、高小山、李子明、王定康等等在方程求解与数学机械化应用方面已得出一系列理论及实际应用的结果。如多元多项因子分解及极限环问题等等，吴文俊在数学机械化方面的各项独创性工作使他在国际、国内产生广泛的影响，享有很高的声誉。单是定理机器证明就已获得许多热情的赞扬。J.S.穆尔（Moore）认为，在吴文俊的工作之前，机械化的几何定理证明处于黑暗时期，而吴文俊的工作给整个领域带来光明。美国定理自动证明的权威人士L.渥斯（wos）认为吴文俊的证明路线是处理几何问题的最强有力的方法，吴文俊的贡献将永载史册[20]。

综合以上对数学机械化史的考察分析，我们可以得出以下三点结论：其一，数学机械化思想来源于中国古算，并从笛卡儿著作中找到根据，其产生和发展经历了从笛卡儿·莱布尼兹等数学家和哲学家的思想奠基，到希尔伯牧定理证明机械化思想从理论上的明确提出，再到定理的机器证明等几个重要的发展阶段。数学机械化走出了一条从公理化出发、通过代数化以达到机械化的道路。其二，数学机械化过程反映了计算和证明这两种基本的数学方法的统一趋势。这是数学家孜孜以求的目标。“在电子计算机广泛应用后形成的现代理论计算机科学看来，任何数学证明。都不过是一种非确定性的计算”。[21]在机器证明中，证明和计算完全结合起来了，能够做到这点则说明了二者本质上的一致性。其三，数学机械化思想从产生到发展的每一阶段，都是建立在对数学更为深刻认识和理解基础上的概念、方法或理论上的突破。对此，中外数学家以及数学大师们各自都为之作出了贡献，而直到吴文俊机械化定理的创立，才为数学的机械化奠定了坚实的基础，致使数学研究的面貌改观。而吴定理植根于中国传统数学这片沃土，从《九章算术》《四元玉鉴》到吴文俊《几何定理机器证明的基本原理》（1984年）中国传统的机械化数学思想清晰可见。随着人们对吴方法、吴定理的认识日益深入，随着吴定理的应用更为广泛，随着其影响逐步扩展，吴的方法和原理越来越受到国际数学界的高度评价。然而，数学机械化的道路毕竟是漫长而艰难的，建立具有中国特色的机械化数学体系依然任重而道远，这有待于致力于此的人们共同努力。

参考文献

[1] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[2] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[3] 李约瑟.中国科学技术史.（第三卷），北京：科学出版社，1987.

[4] 胡作玄.吴文俊//吴文俊主编.世界著名数学家传记.北京：科学出版社，1995：P1774，1774，1775-1776，1777.

[5] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[6] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[7] 吴文俊.对中国传统数学的再认识（下）.百科知识.1987（8）.

[8] 胡作玄.吴文俊//吴文俊主编.世界著名数学家传记.北京：科学出版社，1995：P1774，1774，1775-1776，1777.

[9] 郑毓信等.数学逻辑与哲学.武汉：湖北人民出版社，1987:61.

[10] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[11] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[12] 解恩泽等.数学思想方法.济南：山东教育出版社，1989:50，53.

[13] 见吴文俊.吴文俊文集.济南：山东教育出版社，1986:296，296，38，287，286，286，283.

[14] 解恩泽等.数学思想方法.济南：山东教育出版社，1989:50，53.

[15] 吴文俊.初等几何判定问题与机械化证明.中国科学，1977（6）.

[16] 吴文俊.几何定理机器证明的基本原理.北京：科学出版社，1984:111.

[17] 胡作玄.吴文俊//吴文俊主编.世界著名数学家传记.北京：科学出版社，1995：P1774，1774，1775-1776，1777.

[18] 吴文俊.〈解方程器〉和〈Solver〉软件系统应用举例.数学的实践与认识，1986（2）、（3）.

[19] C.Chou.Mechanical geometry thero-remproving.Reidel，1988.

[20] 胡作玄.吴文俊//吴文俊主编.世界著名数学家传记.北京：科学出版社，1995：P1774，1774，1775-1776，1777.

[21] 洪加威.理论计算机科学的一些问题.自然杂志，1985（2）.

（此文发表于《自然辩证法研究》1997年第10期）