计算机|数学、机器与人类思维，数学是逻辑的还是形式的？

文章插图
从目前机器证明的现状来看，它有两种方向。一是将几何定理证明代数化、解析化；一是将几何定理问题形式化。其实质都是将要解决的问题分解成一些明晰的指令，然后交给机器去执行。这种将问题还原为一套清晰指令的思想最早可以追溯到柏拉图，他把全部推理归约为明晰的规则。
柏拉图之后，在探索人的思维，推理问题这条蜿蜒曲折的道路上，法国著名哲学家、数学家、物理学家、解析几何奠基人之一的笛卡尔为此又跨出了奠基性的一步。17世纪，数学的符号化促发了代数学的发展，也使得计算变得方便和精确。笛卡尔在自己创立解析几何的过程中，通过把几何代数化，不仅大大地扩大了几何的研究领域，而且是使得只有少数天才才能做的几何定理证明成为大家不用奇巧的、神秘的方法就可执行的机械化操作。
逻辑推理能够机械化，就使得人们想到制造机器来实现定理机械化。笛卡尔甚至还最先意识到有限状态机的不充分性，在《演讲录》中，他这样写道∶
虽然这种机器能做许多事. 甚至要比人做得还要好，但是它们确确实实在其他一些方面做不到......因为理性是一种可用在各种各样局势中的普遍工具，而机器的器官必须考虑到每一种特定的行动，按照一种特定的方式安装起来。
笛卡尔将几何代数化的思想，对后来东西方探索定理证明的机械化是一个很大的启发。因为是他从理论上证明了，几何的推理问题可以归结为代数的计算方法问题，而对于计算，当时是有许多方法可供人们使用的，于是几何推理问题通过代数就变得简单、容易。
莱布尼茨与笛卡尔一样，非常重视数学方法的运用，而他自己又酷爱逻辑。在他看来，数学的有效性是由于数学的符号化，而数学中特有的符号语言可为表达思想和进行推理提供很好的条件。因此他力图建立一种精确的、通用的科学语言，以便把人类的一切思想和推理问题转化为数学中的计算，这样思想和推理就会变得像计算一样无可争议。

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

逻辑主义学派（代表人物是罗素）
直觉主义学派（代表人物是布劳威尔）
形式主义学派（代表人物是希尔伯特）。

在形式主义学派纲领中，希尔伯特指出，数学中的全部公理及推理规则可以形式化，于是数学推理就成为一些符号式子之间的变化。而从公理出发，依据所允许的推理规则作变换就几乎成了一种机械的动作。也就是说，由希尔伯特倡导的形式主义学派所导致的数理逻辑的发展，把莱布尼茨等人的理想用精确的数学形式表达了出来。
机器证明
机器证明是指把人证明定理的过程交给计算机去做，也称为定理的机械化证明或自动证明。作为计算机科学领域中的重要课题，它从五十年代中期开始，至今已有半个世纪的发展历史。

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