定理|数学、机器与人类思维，数学是逻辑的还是形式的？( 二 )

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

一是"必须把问题形式化"，即把要求的问题转换成计算机能够接受和处理的形式。（并不是所有的问题都能够形式化）;
二是"问题必须是可计算的"，这里的问题指的是一类而不是个别。所谓可计算的指，能够给出一个统一的机械办法在有限步骤内解决这个问题类中的任何问题。任何一个问题要想用计算机解决，就需要找到一个合适的算法。（有些问题尽管找到了算法，但由于它是按指数时间运行的，所以结果事实上是不可计算的）
三是"问题必须有合理的复杂度"。因为人们经发现有些问题不可能找到一个现实可行的算法。

在形式化方向上，最先进行尝试的是美国工科大学的纽厄尔、肖和西蒙合作编制的一个程序系统，称为逻辑理论程序。该程序模拟人用数理逻辑证明定理的思想，采用分解、代入、替换等规则，证明了怀特海和罗素合著的《数学原理》第二章中的38条定理，到1963年甚至完成了该章中全部定理的证明（52条）。这既是数学机械化路途上的一个里程碑，也是人工智能中的一个里程碑，是计算机模拟人的高级思维活动的一个重大成果。
在代数化方向上进行最先尝试的是中国数学家吴文俊教授，他是在研究中西数学史的时候，深受中国数学算法化特点的启发，发现了一套行之有效的实现数学机械化的方案∶先把即将解决的任意问题转化为数学问题，再转化成代数问题，继而转化为解方程组的问题，最终经消元法而归结为解方程，即几何代数化的方法。
数学实验
数学与自然科学的最大区别是数学里没有实验。在公众中，几乎没有人能够意识到这其实是一个错误的认识。然而事实上，数学实验的历史却与数学本身一样悠久。从中学到大学，我们学习的大部分概念（定义、公理、定理）都是经过几代人的观察、试验和归纳发现的，这种概念的来源方式显然与自然科学中的知识来源是相类似的。大数学家高斯就声称自己获得数学真理的方法是"通过系统的实验"，实际上对于其他的很多数学家也一样。数学的进展都是始于对例子的实验，可是长期以来，数学中的实验成分由于数学家工作的文化环境数学的最终成果都要以证明定理的形式出现，所以证明之前的实验（试验）过程就被掩盖起来。
数学研究对象的特殊性决定了其成果的最终检验不同于自然科学中成果的检验，它的定理不能用实验证实，而必须用逻辑演绎推理证明，所以逻辑证明成为数学研究的一个最大的特点。但是，数学家在发现、证明定理之前，总是要经历一个探索、试验的阶段，即通过对大量的计算和推理进行试探或试验，使个别实例上升为一般猜想；然后再探索证明的思路，这其中当然可能要经过一次一次的反驳或者是遇到反例，最后才获得逻辑上的证明。显然，数学家做出最后证明之前的工作是具有实验性的活动，因此称证明之前的活动为数学实验是非常合理的。
数学实验不同于自然科学中的实验。前者是一种思想实验，而后者是一种实物实验。虽然两种实验的形式不同，但在本质上是一样的（从功能来看）。
数学实验的提出不仅会促进数学的发展，作为一种实验形式，也是科学实验的一种补充。计算机作为计算工具，大家没有疑义。然而作为数学实验工具、定理证明工具，却使大部分人都感到惊疑。首先，人们惊讶数学里竟然有实验，实验向来是于自然科学的。其次，人们怀疑计算机执行实验和定理证明的可靠性。但是无论如何，数学界已经有相当一部分把计算机作为数学研究的实验工具，也有相当一部分人在用计算机证明数学定理，特别地，他们还用计算机发明新的数学定理。