从目前机器证明的现状来看，它有两种方向。一是将几何定理证明代数化、解析化；一是将几何定理问题形式化。其实质都是将要解决的问题分解成一些明晰的指令，然后交给机器去执行。这种将问题还原为一套清晰指令的思想最早可以追溯到柏拉图，他把全部推理归约为明晰的规则。

柏拉图之后，在探索人的思维，推理问题这条蜿蜒曲折的道路上，法国著名哲学家、数学家、物理学家、解析几何奠基人之一的笛卡尔为此又跨出了奠基性的一步。17世纪，数学的符号化促发了代数学的发展，也使得计算变得方便和精确。笛卡尔在自己创立解析几何的过程中，通过把几何代数化，不仅大大地扩大了几何的研究领域，而且是使得只有少数天才才能做的几何定理证明成为大家不用奇巧的、神秘的方法就可执行的机械化操作。

逻辑推理能够机械化，就使得人们想到制造机器来实现定理机械化。笛卡尔甚至还最先意识到有限状态机的不充分性，在《演讲录》中，他这样写道∶

虽然这种机器能做许多事. 甚至要比人做得还要好，但是它们确确实实在其他一些方面做不到......因为理性是一种可用在各种各样局势中的普遍工具，而机器的器官必须考虑到每一种特定的行动，按照一种特定的方式安装起来。

笛卡尔将几何代数化的思想，对后来东西方探索定理证明的机械化是一个很大的启发。因为是他从理论上证明了，几何的推理问题可以归结为代数的计算方法问题，而对于计算，当时是有许多方法可供人们使用的，于是几何推理问题通过代数就变得简单、容易。

莱布尼茨与笛卡尔一样，非常重视数学方法的运用，而他自己又酷爱逻辑。在他看来，数学的有效性是由于数学的符号化，而数学中特有的符号语言可为表达思想和进行推理提供很好的条件。因此他力图建立一种精确的、通用的科学语言，以便把人类的一切思想和推理问题转化为数学中的计算，这样思想和推理就会变得像计算一样无可争议。

机器证明思想的另一个来源是，人们对数学基础中无穷问题的深入研究。对数学基础研究的深入，的成果是引出认识数学性质的三大学派：

逻辑主义学派（代表人物是罗素）

直觉主义学派（代表人物是布劳威尔）

形式主义学派（代表人物是希尔伯特）。

在形式主义学派纲领中，希尔伯特指出，数学中的全部公理及推理规则可以形式化，于是数学推理就成为一些符号式子之间的变化。而从公理出发，依据所允许的推理规则作变换就几乎成了一种机械的动作。也就是说，由希尔伯特倡导的形式主义学派所导致的数理逻辑的发展，把莱布尼茨等人的理想用精确的数学形式表达了出来。

机器证明

机器证明是指把人证明定理的过程交给计算机去做，也称为定理的机械化证明或自动证明。作为计算机科学领域中的重要课题，它从五十年代中期开始，至今已有半个世纪的发展历史。

到目前为止，在机器证明的道路上大致有两个方向，一是代数化，一是形式化。形式化方向的基础是由赫尔勃兰特奠定的，不过他的方法直到1960年才由吉摩尔在计算机上真正实现，而真正在技术上有成就的是美国的纽厄尔、肖和西蒙。代数化方向上做出巨大贡献的是中国科学院院士吴文俊先生。

运用形式化方法实现机器证明，要遵循下面几条原则∶

一是"必须把问题形式化"，即把要求的问题转换成计算机能够接受和处理的形式。（并不是所有的问题都能够形式化）;

二是"问题必须是可计算的"，这里的问题指的是一类而不是个别。所谓可计算的指，能够给出一个统一的机械办法在有限步骤内解决这个问题类中的任何问题。任何一个问题要想用计算机解决，就需要找到一个合适的算法。（有些问题尽管找到了算法，但由于它是按指数时间运行的，所以结果事实上是不可计算的）

三是"问题必须有合理的复杂度"。因为人们经发现有些问题不可能找到一个现实可行的算法。

在形式化方向上，最先进行尝试的是美国工科大学的纽厄尔、肖和西蒙合作编制的一个程序系统，称为逻辑理论程序。该程序模拟人用数理逻辑证明定理的思想，采用分解、代入、替换等规则，证明了怀特海和罗素合著的《数学原理》第二章中的38条定理，到1963年甚至完成了该章中全部定理的证明（52条）。这既是数学机械化路途上的一个里程碑，也是人工智能中的一个里程碑，是计算机模拟人的高级思维活动的一个重大成果。

在代数化方向上进行最先尝试的是中国数学家吴文俊教授，他是在研究中西数学史的时候，深受中国数学算法化特点的启发，发现了一套行之有效的实现数学机械化的方案∶先把即将解决的任意问题转化为数学问题，再转化成代数问题，继而转化为解方程组的问题，最终经消元法而归结为解方程，即几何代数化的方法。

数学实验

数学与自然科学的最大区别是数学里没有实验。在公众中，几乎没有人能够意识到这其实是一个错误的认识。然而事实上，数学实验的历史却与数学本身一样悠久。从中学到大学，我们学习的大部分概念（定义、公理、定理）都是经过几代人的观察、试验和归纳发现的，这种概念的来源方式显然与自然科学中的知识来源是相类似的。大数学家高斯就声称自己获得数学真理的方法是"通过系统的实验"，实际上对于其他的很多数学家也一样。数学的进展都是始于对例子的实验，可是长期以来，数学中的实验成分由于数学家工作的文化环境数学的最终成果都要以证明定理的形式出现，所以证明之前的实验（试验）过程就被掩盖起来。

数学研究对象的特殊性决定了其成果的最终检验不同于自然科学中成果的检验，它的定理不能用实验证实，而必须用逻辑演绎推理证明，所以逻辑证明成为数学研究的一个最大的特点。但是，数学家在发现、证明定理之前，总是要经历一个探索、试验的阶段，即通过对大量的计算和推理进行试探或试验，使个别实例上升为一般猜想；然后再探索证明的思路，这其中当然可能要经过一次一次的反驳或者是遇到反例，最后才获得逻辑上的证明。显然，数学家做出最后证明之前的工作是具有实验性的活动，因此称证明之前的活动为数学实验是非常合理的。

数学实验不同于自然科学中的实验。前者是一种思想实验，而后者是一种实物实验。虽然两种实验的形式不同，但在本质上是一样的（从功能来看）。

数学实验的提出不仅会促进数学的发展，作为一种实验形式，也是科学实验的一种补充。计算机作为计算工具，大家没有疑义。然而作为数学实验工具、定理证明工具，却使大部分人都感到惊疑。首先，人们惊讶数学里竟然有实验，实验向来是于自然科学的。其次，人们怀疑计算机执行实验和定理证明的可靠性。但是无论如何，数学界已经有相当一部分把计算机作为数学研究的实验工具，也有相当一部分人在用计算机证明数学定理，特别地，他们还用计算机发明新的数学定理。

从总体上看，数学是由定义、概念、逻辑规则、定理、证明、推论等一系列的演绎模式组成的严密的、抽象的体系。可是具体地回想我们做几何定理证明的全过程，就会意识到这个严密的体系其实是呈现给大家的最后结果。而在这个结果之前，还不知道要做多少回的试验。比如在证明一个几何定理时，为了寻找那条辅助线，我们总是在这个方向上比一比，在那个方向上画一画，猛然间找到了那一条合适的辅助线，还觉得是一种幸运。

持续了20多个世纪的信念——数学是演绎的，正在遭到动摇，这一巨大变化是计算机引起的。但是应该指出的是，计算机是使得数学中的实验成分被突显出来，因为事实上数学是具有实验性的一面，而不是因为有了计算机才有了数学实验。正如一些人已经指出的，计算机在数学中的应用只是扩大了数学实验的规模。

总之，我们说在严密、抽象的数学背后，有着一个很漫长的试验过程，而这个过程在数学的最终成果表达中被隐去了。久而久之，就给人们造成了一种错觉，数学就是非常人所能研习的抽象的演绎科学。但是现在计算机把数学中的这一实验工作阶段的重要性显示出来。

数学实验是按照程序设计，在思维中进行的一种特殊的论证方式。要进行数学实验，先是要建立数学模型，因为数学实验是对数学模型的一种实验。它既不同于在自然科学中的实物实验，也不同于逻辑中的形式推理。对于实物实验来说，它需要借助于物质的手段，进行实际的操作和测量，然后再做数据处理，最后分析整个实验过程;而对于逻辑中的形式推理，则是借助于语言进行形式的变换。但是数学中的实验与自然科学中的实验在功能上是相同的∶都是在一次又一次的试验中获得所需要的结论。

在数学实验之后，不管是得到的猜想还是进一步验证的猜想，一定要给出数学上的逻辑证明。这是数学与其他自然科学的本质差别之所在，也是它自己保持正确的必要手段。在实验中无论得到的猜想多么漂亮、多么有用，如果没有一个严格的证明，它就永远不能被数学界承认。当然就目前数学的现状而言，你可以给出像过去那样的演绎证明，也可以给出像解决四色问题、机器定理证明那样的计算机证明。

在计算机上进行数学实验，必须要做程序设计方案。数学实验中的程序设计与一般采用的固定地重复某些运算步骤的方法是不同的。确切地说，它所做的程序设计并不给出机器每一步怎么，而只是给出机器所要遵循的原则和规律。举例来说，从甲地乘车到乙地，不是事先规定你必须从甲地乘坐某次车，中途再换乘某次车，最后怎样到达乙地;而是给出甲地和乙地的地理位置、交通干线和车辆的流通情况，至十具体乘哪班车，需根据有关情况随机判断和选择。也正是这个意义上，机器可作为进行数学研究的实验工具。实践表明，借助计算机的判断和选择能力，通过实验可以启发数学家的思维，从而使一些问题得到解决。