数学思想方法的重大突破分析

　　一、机器证明的必要性和可能性

数学思想方法的重大突破分析

　　定理机器证明的出现不是偶然的，而是有其客观必然性，它既是电子计算机和人工智能发展的产物，也是数学自身发展的需要。

　　首先，现代数学的发展迫切需要把数学家从繁难的逻辑推演中解放出来。我们知道，任何数学命题的确立都需要严格的逻辑证明，而数学命题的证明是一种极其复杂而又富有创造性的思维活动，它不仅需要根据已有知识和给定条件进行逻辑推理的能力，而且常常需要相当高的技巧、灵感和洞察力。有时为寻找一个定理的证明，还需要开拓一种全新的思路，而这种思路的形成竟要数学家们付出几十年、几百年乃至上千年的艰苦努力。如果把定理的证明交给计算机去完成，那就可以使数学家从冗长繁难的逻辑推演中解放出来，从而可以把精力和聪明才智更多地用于富有开创性的工作，诸如建立新的数学概念，提出新的数学猜想，构造新的数学命题，创造新的数学方法，开辟新的数学领域等等，由此提高数学创造的效率。

　　其次，机器证明的必要性，还表现在数学中存在着大量传统的单纯人脑支配手工操作的研究方法难以奏效的证明问题。这些问题往往因为证明步骤过于冗长，工作量十分巨大，使数学家在有生之年无法完成。电子计算机具有信息储存量大，信息加工及变换的速度快等优越性，这就突破了人脑生理机制的局限性与时空障碍。也就是说，如果借助电子计算机的优势就有可能使某些复杂繁难的证明问题得以解决。“四色猜想”的证明就是一个令人信服的范例。“四色猜想”提出于19世纪中叶，它的内容简单说来就是：对于平面或球面的任何地图，用四种颜色，就可使相邻的国家或地区区分开。沿着传统的手工式证明的道路，数学家们做了各种尝试，结果都未能奏效。直到1976年，由于借助于电子计算机才解决了这道百年难题。为证明它，高速电子计算机花费了120个机器小时，完成了300多亿个逻辑判断。如果这项工作由一个人用手工去完成，大约需要30万年。

　　第三，机器证明的可能性，从认识论上看，是由创造性工作和非创造性工作之间的关系决定的。我们知道，在定理的证明过程中，既有创造性思维活动，又有非创造性思维活动，而思维活动中的创造性工作和非创造性工作并不是完全割裂的，而是互为前提、相互制约、相互转化的，非创造性工作是创造性工作的基础，创造性工作又可以通过某种途径部分地转化为非创造性工作。当我们通过算法程序把定理证明中的创造性工作转化为非创造性工作之后，也就有可能把定理的证明交给计算机去完成。

　　第四，理论上的研究已经表明，的确有不少类型的定理证明可以机械化，可以放心地让计算机去完成。希尔伯特和塔尔斯基的机械化定理，就是对定理证明机械化可能性的一种理论探讨。吴文俊教授对几何定理证明机械化的可能性曾作过深入的研究。他将可施行机械化证明的实现划分为三种不同的类型，并给出了实现机器证明的一个行之有效的一般方法。这个一般化方法的基本思想是：首先借助坐标系，把定理的假设与求证部分用一些代数关系式来表示，然后再把表示代数关系的多项式做适当处理，即把终结多项式中的坐标逐个消去，当消去的结果为零时，定理也就得证。

　　目前，机器证明作为数学研究的一种方法，还存在着许多理论和技术上的问题，这些问题的解决将有待于算法理论、计算机科学和人工智能等各个领域出现新的重大突破。

　　二、机器证明的兴起和进展

　　机器证明的思想渊源可追溯到几何代数化思想的出现，然而历史上最先从理论上明确提出定理证明机械化思想的是希尔伯特。1899年，他在《几何基础》这部经典名著中指出，初等几何中只涉及从属平行的定理可以实现证明的机械化，他还提出了有名的“希尔伯特机械化定理”。希尔伯特的几何机械化思想遵循的就是一条几何代数化的道路：从公理系统出发，建立坐标系，引进数系统，把几何定理的证明转化为代数式的计算。这是一条从公理化走向代数化直至数值化的道路。1950年，波兰数理逻辑学家塔尔斯基进一步从理论上证明，初等代数和初等几何的定理可以机械化。他还提出了以他的名字命名的机械化定理以及制造证明机的设想。

　　机器证明史上的第一项奠基性的突破，是由美国的卡内基大学—兰德公司协作组做出的。1956年，这个协作组的西蒙、纽厄尔和肖乌等人在电子计算机上成功地证明了罗素和怀特海所著的《数学原理》第二章52条定理中的38条。这一年可作为历史上计算机证明定理的开端。1963年，他们又在计算机上证明了全部52条定理，西蒙等人使用的是LT（逻辑理论机）程序。这种程序不是刻板的固定算法程序，而是使用了心理学方法，将人脑在进行演绎推理时的逻辑过程、所遵循的一般规则和所经常采用的策略、技巧，以及简化步骤的一些方法等编进计算机程序，让计算机具有自己去探索解题途径的某种能力。这一程序为机器证明提供了一个切实可行的算法，通常称它为“启发式程序”。

　　在机器证明的开拓者中，还有著名的美籍华人王浩教授。1959年，他只用9分钟的机器时间，就在计算机上证明了罗素和怀特海《数学原理》一书中的'一阶逻辑部分的全部定理350多条，在当时数学界引起了轰动。

　　改进算法程序是提高机器证明效率的一个重要方面。在这方面，美国数学家鲁滨逊首先取得了重大突破。1965年，他提出了有名的归结原理。这一原理的基本出发点是，要证明任何一个命题为真，都可以通过证明其否定为假来得到。它要求把问题用一阶逻辑表示出来，并且变为只具有永真式或永假式性质的公式。由于许多定理都可以在一阶逻辑中得到表示，因而这一程序具有较大的实用性，对提高机器证明的效率有着重要的方法论意义，大大地推动了机器证明的研究。

　　70年代，机器证明得到新的重大进展。1976年，美国数学家阿佩尔和黑肯借助计算机成功地解决“四色猜想”的证明问题。这是机器证明首次解决传统人脑支配手工操作所长期没能解决的重大问题。1971-1977年间，莱得索等人给出了分析拓朴学和集合论方面的一些著名定理的机器证明。1979年，波依尔和穆尔等人作出了递归函数方面的机器证明系统。

　　我国数学家在机器证明研究上取得了显著的成果，引起了国内外学术界的关注。1977年，吴文俊教授证明了初等几何主要一类定理的证明可以机械化。1980年，他还用一部微机在20和60个机器小时左右分别发现了两个几何学的新定理。吉林大学和武汉大学的研究人员也在定理的机器证明方面取得了许多可喜的成果。

　　上面我们考察和分析了数学史上发生的6次重大突破。除了这6次重大突破外，还有许多重大事件也都具有一定的突破性，它们都不同程度地带来了数学思想方法的重大变化。如非欧几何的发现，群论的产生，勒贝格积分的建立，突变理论的出现，非标准分析的诞生，就是这样的事件。现代科学技术革命的兴起，向数学提出了一系列新的重大课题，可以预想，对这些课题的探讨，必将会引起数学在思想方法上发生新的重大突破，使数学的面貌发生新的改观。

【数学思想方法的重大突破分析】相关文章：

重大突破思想方法常量变量学到数学05-12

数学思想方法06-26