数学机械化

出处：按学科分类—自然科学总论 北京出版社《现代科技综述大辞典上》第119页（3328字）

数学操作的机械化分解，使之成为简单的、单调的、刻板的、重复的动作组合，这样就可以用计算机处理、解决大量的数学问题。

中国古代数学基本上是一种机械化的数学。秦汉时期的《九章算术》，其中对四则运算、开方的机械化算法过程有详细说明，对于线性方程组的解法在魏晋时期的刘徽所写的《九章算术注》中就已说明了几种机械化的消去法及其详细的机械算法过程。到宋代更发展到了高次代数方程求数值解的机械化算法。求解同余式的问题，秦九韶在其《数书九章》中曾给出了“大衍求一术”的算法，其机械化程序非常之高。数学的机械化主要是几何学机械化，而几何学机械化方法起源于12世纪和13世纪中国宋元时期初次出现的几何学代数化，即将几何学问题化为多项式问题，以及相伴而生的多项式组消去法。

17世纪德国莱布尼兹(G．W．Leibniz)曾有过“推理机器”的机械化证明的设想。

只是直到19世纪末德国希尔伯特(D．Hilbert)以及后来建立的数理逻辑，才使这一问题具有明确的数学形式。几十年来数学家们为解决这一问题付出了巨大劳动，但是他们所得到的结果基本上是反面的，即所谓不可判定性。例如有：哥德尔(K．Gödel)定理：初等整数数论的定理证明不可能机械化。随着电子计算机的问世，使证明机械化这一设想有了现实的意义。

1950年波兰塔斯基(A．Tarski)证明了一个值得称道的正面结果——塔斯基定理：初等几何(以及初等代数)的定理证明可以机械化。塔斯基等人还因此提出制造判定机器(也就是证明机)的设想。

然而他们的方法与设想基于斯图模(C．F．Sturm)定理的某种推广，而且这些方法极繁复，实际上计算机难以实现。

1956年以来，美国科学家开始尝试用电子计算机证明一些数学定理，1959年美国王浩设计了相应的程序，用计算机证明了罗素(B．A．W．Russell)、怀德海(H．Whitehead)的巨着《数学原理》中的几百条定理，仅用9min。1976年，美国阿佩尔(K．Appel)和哈肯(W．Haken)在高速电子计算机上用1200h的计算时间证明了“四色定理”，使100多年来未能解决的这个难题得到了肯定的回答。

另一个被忽视的正面结果，是由希尔伯特在1899年提出的“希尔伯特机械化定理”：初等几何中只涉及关联与平行关系的定理证明可以机械化。显然这是塔斯基定理的一个特例，但值得注意的是，希尔伯特的机械化证明方法是切实可行的。

中国吴文俊在中国古代数学机械化思想的启发下，独立研究并于1977年获得了下面的结论：

定理1 初等几何中只牵涉到关联、平行与合同关系的定理证明可以机械化。

这与希尔伯特不谋而合。同时吴文俊还对所需计算量作出了理论上的估计，得到：

定理2 初等几何中只牵涉关联、平行与合同关系且“不可约”的定理证明，其计算量满足不等关系：计算复杂度≤定理复杂度·几何复杂度。

1978年，吴文俊又将初等几何的结果推广至初等微分几何，得到：

定理3 在初等微分几何中，凡可用微分多项式等式关系表达的定理的证明可以机械化。

只是这里定理证明的机械化方法依赖于里奇(G．RicciCurbastro)关于微分方程与微分代数的理论与方法，比用初等几何的情形要复杂得多。

吴文俊提出的新的机器证明方法被称为“吴方法”，它是基于Ritt原理和零点分解定理的。吴文俊、周咸青、王浩、胡森和王东明等人，使用吴方法在微机上迅速地解决下述各问题：(1)初等几何定理的机器证明与机器发明。

如1989年周咸青基于吴方法用自己编制的程序，在计算机上证明了512条定理；所用的机器时间一般每条定理才几秒钟，其中还有许多新定理。这种方法还普遍适用于各种初等几何，其中包括非欧几何、圆几何等。(2)微分几何定理的机器证明与机器发明。(3)未知关系的机械推导。

(4)高次代数方程组求解问题。(5)因子分解问题(特别是对多变量多项式的因子分解)。

举世瞩目的吴方法可以分成下面3个主要步骤证明几何命题：第1步，把几何命题化为纯代数问题。第2步，将几何命题假设部分的代数关系式进行整理，然后依确定步骤验证命题终结部分的代数关系式是否可以从假设部分已整理成序的代数关系式中推出。它包括：(1)整序。即是把假设部分化成一种规范形式——吴升列。(2)伪除法求余。最后得到的多项式R0，如果R0是零多项式，就表明在非退化条件下，所要检验的命题成立。

这由吴方法中一条定理所保证。而如果R0不是零多项式，吴方法证明(i)若相应的升列是“不可约”的，则R0≠0便表明命题不成立。

(ii)对“可约”的升列，则总可以通过因式分解，分解为几个“不可约”的升列，从而把问题完全解决了。第3步，依据第2步中所确定的步骤编程序，并在计算机上实施，以得出命题是否成立的最后结论。

吴方法的出现，开辟了数学机械化的一个新纪元，用它不但证明牛顿定律可以用计算机程序从开普勒定律推导出来，而且也在机器人学、自动控制、计算机视觉、化学平衡、几何模型等领域有着广泛的应用。吴方法大有方兴未艾之势，这一领域中有许多有意义的课题尚待解决。如(1)几何不等式的证明机械化。(2)非退化条件的处理方式，尚有争论。

(3)可约系统的更有效算法。

(4)如何把研究范围从多项式推广到初等函数。(5)怎样设计并行程序，用作处理更繁难的问题。

在吴文俊数学机械化理论与方法的影响下，1986年以来中国洪加威等人又提出了通过数值实例的检验来证明几何定理的思想与方法，这一方法在机器证明领域是一很有前景的研究热点。

。【参考文献】：

1 Tarski A．A decision method for elementary algebra and geometry，1951

2 Wang Hao．IBM J Res Dev，1960，4：2～22

3 吴文俊．中国科学，1977，6：507～516

4 吴文俊．科学通报，1978，523～524

5 Wu Wen-tsun．Automated．Theorem proving：AMS，1983，235～242

6 吴文俊．几何定理机器证明的基本原理．北京：科学出版社，1984

7 吴文俊．吴文俊文集．济南：山东教育出版社，1986，280～387

8 Shang-Ching Chou．Mechanical Geometry Theorem Proving D Reidel Publishing Company，1988

9 井中．自然杂志，1990，10：682～688

10 吴文达．中国科学院院刊，1991，1：39

(安徽机电学院王庚副教授撰；胡炳生审)