爱华网一、机器证明：古老的梦想
相传 Ptolemy 王曾向 Euclid 请教学习几何的捷径， Euclid没有屈从帝王的尊严，直率地说：几何中无王者之路 ( There is no royalway in geometry ) 。
以希腊的几何学为代表的古代西方数学，其特点是在构造公理体系的基础上证明各式各样的几何命题。几何题的证法，各具巧思，争奇斗艳，无定法可循，只有依赖个人的经验、技巧和灵感。学习几何的孩子做梦都在想：要是几何题象解一元二次方程那样多好。这种愿望由来已久，17 世纪法国的数学家 Descartes曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。”Descartes把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方程求解是可以机械化的。但Descartes没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，实现了初等几何问题的代数化。
比 Descartes 晚一些的德国数学家 Leibnize曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。Leibnize认为，他的方案一旦实现，人们之间的一切争论都可以被心平气和的机器推理所代替。他的努力促进了Boole代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。
更晚一些，德国数学家 Hilbert明确提出了公理系统中的判定问题：有了一个公理系统，就可以在这个系统基础上提出各式各样的命题，那么，有没有一种机械的方法，即所谓算法，对每一个命题加以检验，判明它是否成立呢？正是在Hilbert的名著《几何基础》一书中就提供了一条可以对一类几何命题进行判定的定理— 当然，在那个时代，不仅 Hilbert本人，整个数学界都没有意识到这一点。
数理逻辑的研究表明， Hilbert 的要求太高了。著名的 Godel不完全定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！
数学大师们坚持不懈地求索，表明数学机械化的思想重要而深刻；而数学机械化在历史上发展缓慢，同时也意味着这一方向道路漫长而艰难。
证明的机械化，如果没有可以进行数学演算的机器，只能是纸上谈兵。电子计算机的问世，促使数学机械化的研究活跃起来。波兰数学家Tarski 在 1950 年推广了关于代数方程实根数目的 Sturm法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。
1959年，著名数理逻辑学家，美国洛克菲勒大学王浩教授设计了一个程序，用计算机证明了Russell 、 Whitehead的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了 9分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。特别的是，他第一次明确提出“走向数学的机械化”（Toward Mechanical Mathematics ）。 1976年，美国两位年轻的数学家在高速电子计算机上耗费 1 200小时的计算时间，证明了“四色定理”，使数学家们 100年来未能解决的难题得到肯定的回答。
在数学发展的漫长历史中，积累了无数的几何定理。这里面有许多巧夺天功、趣味隽永的杰作。由于传统的兴趣和应用的价值，初等几何问题的自动求解遂为数学机械化的研究焦点。自Tarski 的引人注目的定理发表以来，已经 26年过去了，初等几何定理的机器证明，仍然没有令人满意的进展。在经过许多探索和失败之后，人们在悲叹：光靠机器，再过100 年也未必能证明出多少有意义的新定理来！
吴文俊的工作，揭开了机器证明领域的新的一页。
二、吴方法：王者之路
当中国的历史艰难地走出十年浩劫的磨难的时候， 1977年，吴文俊在《中国科学》上发表的论文《初等几何判定问题与机械化问题》，为数学机械化领域送去了一缕清新的春风。1984年，吴文俊的学术专著《几何定理机器证明的基本原理》由科学出版社出版，这部专著遵循机械化思想引进数系和公理，依照机械化观点系统地分析了各类几何体系，明确建立了各类几何的机械化定理，着重阐明几何定理机械化证明的基本原理。1985年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。这篇重要文献，是正式建立求解多项式方程组的吴文俊消元法的重要标志。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的学术路线。自此，“吴方法”宣告诞生，数学机械化研究揭开了她新的一幕。
几何问题的代数化是几何问题机械化的第一步，为此需要引进数系，建立坐标系，把几何命题的图中的各种关系利用代数方程来描述。在适当选取坐标系后，如果几何定理的假设条件可表示为一组代数方程[H] ： f 1 = 0 ， f 2 = 0 ， …， f r= 0 ，而几何定理的结论由代数方程C : g = 0 所刻画，这里 f 1 , f 2 ,… , fr 和 g 都是变元 x 1 ,x 2 ,…,x n的多项式，那么几何定理的机械化证明就归结为如下问题：
机械化问题构造并提供一种确定的、机械的算法，使得依此算法进行有限步之后即可判定：在若干附加条件之下，结论C 是否可由假设 [H] 推出，即是否可由 f 1 = 0 ， f 2= 0 ， ……
f r= 0 推出 g = 0 。
由此可见，实现数学定理机械化证明的关键，在于必须对表示定理假设的多项式组[H] 的零点集给出构造性的描述 , 以便区分多项式组 [H] 的零点集 ,从而可以确定在多项式组 [H] 零点集的哪部分之中 , 能够保证多项式g =0.吴文俊消元法（吴方法）恰恰完成了这项任务。因此，吴方法是定理机器证明吴文俊原理的理论基础，定理机器证明的机械化原理的建立是吴方法的成功运用。
吴文俊原理 设数学定理的假设条件由多项式方程组[H] ＝ 0 表示，定理的结论由多项式方程 g =0 表示。并设 CS＝ {A 1,A 2,….,A k} 为多项式方程组 [H] 的特征列。如果多项式g 对 [H] 的特征列 CS 的余式 R=0, 则在条件 I i ≠0, i=1,2,…,k 之下 , 可从 [H]=0 推出 g =0 。
条件 I i ≠ 0, i=1,2,…,k称为数学定理成立的非退化条件。这组非退化条件是在计算特征列过程中自动产生的。非退化条件这一概念的发现, 是吴文俊在数学机械化证明领域的突出贡献。这一概念的引进 ,实现了数学定理机器证明的决定性突破。
一般说来 , 用吴方法判定一个命题 , 要分三步进行 :第一步是把所给命题化为代数形式，即判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题; 第二步是整序，即把刻划命题条件的多项式组 [H] 经整序化为升列 AS；第三步是求余，即将刻划命题结论的多项式 g 对于升列 AS约化求取余式 R 。 若 R=0 ，即可断定命题在非退化条件 I i ≠0, i=1,2,…,k 之下成立，或者说命题一般成立，其中 I 1, I 2,…, I k是升列 AS 中各多项式的初式。若 R 不为 0, 则当 AS 为不可约升列时 ,可断定命题不真。
多项式方程组求解曾被认为是极为困难的问题 ,这已为它的研究历史过程所证明。但是 ,吴文俊消元法的叙述简明自然，顺理成章，结论易懂，方法易学。可以用相当短的时间向初学者介绍吴方法，并在计算机上具体操作吴方法的计算过程。初学者往往惊奇的发现：吴方法竟是这样的简单自然，感叹为什么别人没有发现它！事实上，将公认的难题，应用初等方法简朴自然地加以解决，是数学科学返璞归真的最高境界。
三、《九章算术》：惟有源头活水来
50年代，拓扑学刚刚从艰难迟缓的发展中走向突飞猛进，吴文俊敏锐地抓住了拓扑学的核心问题，在示性类与示嵌类的研究上取得了国际数学界交相称誉的突出成就。1956 年荣获国家自然科学一等奖， 1957年当选为中国科学院学部委员（现称院士）。那时他才 38岁。作为一位年轻的数学家，这已是莫大的荣誉了。而对吴文俊来说，这只是在西方人开创的方向上做出的工作，新中国的数学家应该开拓出属于自己的研究领域。
但是，路在何方呢？那就是数学机械化！是什么力量使得吴文俊从一位卓有成就的拓扑学家，走上数学机械化的研究道路呢？吴文俊在《吴文俊文集》前言中有过动情的叙述：
作者关于机械化思想的形成，决非一朝一夕，至少在 70年代以前，机械化的概念在作者脑海里还毫无踪影。经过对中国古代数学的学习和触发，结合着几十年来在数学研究道路上探索实践的回顾与分析，终于形成了这种数学机械化的思想。这种思想一旦形成，就自然地化成一股顽强的动力。十几年来，作者一直在这一方向道路上摸索前进，艰苦奋斗，义无反顾。
70年代初，吴文俊开始研读中国数学史。中国古代数学曾有过辉煌的历史，直到14世纪，在许多数学领域都保持西方望尘莫及的水平。但是，西方一些数学史家不了解也不承认中国古代数学的光辉成就，将其排斥于“数学主流”之外。吴文俊对此作了正本清源的研究。1975年，他撰写了《中国古代数学对世界文化的伟大贡献》，文中详细列举在代数、几何、三角、解析几何和微积分等学科的发现和创立过程中，中国传统数学所起的重大作用，吴文俊认为：近代数学之所以能够发展到今天，主要是靠中国的数学，而非希腊的数学，决定数学历史发展进程的主要是中国的数学而非希腊的数学。这一论断在当时真可谓空谷惊雷，振聋发聩。此后，吴文俊对中国数学史的研究一发而不可收。大约在 1976年，他的论文《我国古代测望之学重差理论评价—兼评数学史研究中某些方法问题》洋洋洒洒3 万余言，列举参考文献达 48种，从古代“重差理论”入手，见微知著，批判了数学史研究中“以今代古”所产生的巴比伦神话、印度神话以及丢番图神话；正是在此文中，吴文俊意识到“几何与代数的配合、代数的几何应用与几何的代数化正是宋元天元术的主要含义”，指出“在宋元数学家的手里为了发展天元术而建立了一整套的代数机器”。这为他日后机器证明思想埋下了伏笔。随后的另一篇文章《〈海岛算经〉古证探源》，提出了古证复原的三项原则，在数学史界引起了强烈反响。1986 年，吴文俊应邀在国际数学家大会做 45分钟报告，作为国际著名的数学家，吴文俊的报告却是“近年来中国数学史的研究”。吴文俊热情讴歌中国古代数学的代表作《九章算术》。在他主编的《〈九章算术〉与刘徽》的前言中，他写到：“《九章算术》是我国数学方面流传至今最早也是最重要的一部经典著作。它承前启后，一方面总结了秦汉以前的数学成就，另一方面又成为汉代以来达两千年之久数学研究与创造的源泉。特别是三国时期刘徽的《九章算术注》，对数学理论多所阐发，影响深远。总之，《九章算术》与刘徽《九章算术注》，对数学发展在历史上的崇高地位，足以与古希腊的欧几里得《几何原本》东西辉映，各具特色”。他进一步指出：“作为一名中国的数学工作者，首先应该对自己的数学历史有深刻的认识，为此必须首先对《九章算术》与刘徽《九章算术注》有确切的了解。”“要预见数学的将来，不能不研究《九章算术》与《九章算术注》所蕴含的深邃的思想在数学发展过程中的历史功绩，也不能不正视正在展露头角的这种思想对数学现状的影响”。
吴文俊以一位数学家的素养敏锐地感受到中国传统数学“寓理于算”鲜明特点表现在它的机械化和构造性，他在论文《从〈数书九章〉看中国传统数学构造性与机械化的特色》中着力阐明了这一点。后来在为数学史家李继闵先生的著作《〈九章算术〉及其刘徽注研究》作序时，他把自己多年研究数学史的体会系统完整地表述出来，他指出：
我国传统数学在从问题出发以解决问题为主旨的发展过程中建立了以构造性与机械化为其特色的算法体系，这与西方数学以欧几里得《几何原本》为代表的所谓公理化演绎体系正好遥遥相对。《九章》与《刘注》是这一机械化体系的代表作，与公理化的代表作欧几里得《几何原本》可谓东西辉映，在数学发展的历史长河中，数学机械化算法体系与数学公理化演绎体系曾多次反复互为消长，交替成为数学发展中的主流。肇始于我国的这种机械化体系，在经过明代以来近几百年的相对消沉后，势必重新登上历史舞台。《九章》与《刘注》所贯穿的机械化思想，不仅曾深刻影响了数学的历史进程，而且对数学的现状也正在发扬它日益显著的影响。它在进入21 世纪后在数学中的地位，几乎可以预卜。
也就是在这个时期，吴文俊到计算机工厂劳动，通过接触计算机，切身体会到了计算机的巨大威力，敏锐地觉察到计算机有极大的发展潜能。他一头扎进机房，从HP-1000机型开始，学习算法语言，编制算法程序。就这样，中国数学史的启发，“玩”计算机的感受，更是几十年在数学研究道路上的探索与实践，终于在吴文俊的脑海里升华为数学机械化的思想。1977年，吴文俊的论文《初等几何判定问题与机械化证明》发表于《中国科学》，吴文俊特地为此文写了一个附注，阐明机械化思想起源：
我们关于初等几何定理机械化证明所用的算法，主要牵涉到一些多项式的运用技术，例如算术运算与简单消元法之类。应该指出，这些都是12 至 14 世纪宋元时期中国数学家的创造，在那时已由相当高度的发展。… 事实上 , 几何问题的代数化与用代数方法系统求解 ,乃是当时中国数学家主要成就之一 , 其时间远在 17世纪出现解析几何之前。
吴文俊汲取中华民族灿烂文化之精华，发扬中国古代数学的优良传统，创造了世所公认的机器证明的“吴方法”，彻底改变了数学机械化领域的面貌。吴文俊的卓越建树，生动的证明了这样一个真理：正确认识和研究数学的历史，不仅是数学发展的必然要求，也是一个数学家永葆学术青春的重要源泉之一。
四、数学机械化：无尽的前沿
Fourier曾有过这样的名言“对自然的深入研究，是数学发现最丰富的源泉”。然而，这还是不够的，还应该加上这样的续言：数学内容的不断丰富和在更深层次的成熟发展，必然对自然界的认识、理解和改造产生更大的作用。
吴文俊所倡导的数学机械化研究，一方面继承了古代中国数学思想的精华，一方面适应了现代科学技术的发展。数学机械化的研究最先在几何定理机器证明取得了突破性的成果，随着时间的推移、工作的积累和方向的拓展，数学机械化必将为中国乃至世界数学的发展做出积极的贡献，也必将使数学更好地为科学技术服务，尤其是为高科技提供理论武器和有效的工具。从几何的机器证明到内容更为丰富的数学机械化是一种必然的趋势。这里采撷几朵绚丽的奇葩，以展示数学机械化的应用和它对当代高科技的影响。
物理规律的发现数学在解释物理现象、解决物理问题方面所处的重要地位是毋庸置疑的。今天，科学家们对于借助计算机和数学理论来发现物理规律的热情依旧不减。
在科学史上， Newton 通过观测和试验从 Kepler定律导出万有引力定律是一个重要的历史事件。但是如何通过理论推导来重现Newton的伟大发现，这一点在现行的教科书里几乎没有触及。相反地，教科书中大量介绍了如何从Newton 定律推导 Kepler 定律。
1986 年吴文俊访问美国 Argonne 国家试验室， Gabriel教授正为如何借助计算机和数学工具，从 Kepler 定律推导出 Newton定律而绞尽脑汁。回国后，吴文俊用自己的方法，通过计算机，完成了这一推导工作，并因此博得了许多科学家的称赞。国际自动推理研究领域的著名科学家，Argonne 实验室的 Wos教授认为，吴的这一贡献对自动定理证明领域是一次极为重要的拓广，表现了吴的非凡的洞察力和卓越的智慧。进一步的工作揭示，假设对Newton 定律一无所知，仅仅从 Kepler定律的微分代数方程描述出发，经过整序运算，计算机自动产生了新的微分代数表达式，再加上一些技术性的分析，可以得到表达Newton 定律的微分代数表达式蕴含在其中——也就是说，在假设 Kepler定律的前提下，用计算机自动地发现了 Newton 定律， Newton多年的心血，现在只需一刻钟的功夫，就重现于眼前，这真是一个激动人心的结果！
机器人与机构学机器人的制造是多学科共同发挥作用的复杂的系统工程。工业机器人的主体基本上是一只类似于人的上肢功能的机械手臂，或是无关节结构，或是关节式结构。如果要在三维空间对物体进行作业，一般则需要具有六个自由度，即沿三个坐标轴的直线移动和绕这三轴的转动。例如，PUMA560机器人，就是六自由度关节型电动机械手臂。对于这个具体的机器人，求解运动学方程，就是要决定各关节应转动的角度q 1 , q 2 ,…, q 6 , 分别是多少 ?这需要解一组非线性方程组如果采用数值迭代方法，求解过程很慢，同时也不能保证求出所有的解。一个自然的问题就是能否找出q i 的封闭解。虽然就 PUMA560来说，封闭解已被决定，但是对于一般的 PUMA型机器人时，用吴文俊方法，依然可以求出特征列意义下的封闭解。而这是以往的方法很难达到的。
机构学是现代各种机械设计的基础，平面机构运动学分析与综合又是机构学的基础。此类问题研究主要是依据德国学者L.Burmester 所建立的运动几何学方法 ,按照这个理论，平面机构综合问题有图解法和解析法两类。图解法过程繁复，工作量很大且不精确；解析法建模复杂，求解也复杂；若用数值法求解，又不易得到全部解。现在，借助于吴文俊整序方法，这类问题已获得了特征列形式的封闭解。
计算机科学中的应用数学机械化在中国得以迅速发展，一个很重要的因素是计算机的介入。现在，一个可喜的良性循环已经形成，即数学机械化对于促进计算机科学自身的发展，对于计算机科学中的一些应用领域都产生了积极的影响,形成了投桃报李的局面。计算机视觉是一个重要的应用研究领域。这一方面，任何有意义的新结果，必然会促进机器人的发展。1988 年和 1991 年，纽约大学的 Kapur 教授和通用电气公司的 Mundy博士，敏锐而快速的把中国人创立和发展的特征列方法引入高科技的应用当中。用Mundy博士自己的话“最近我们发觉把吴文俊三角化方法和求根技术结合起来，可以形成解非线性约束问题的有效方法。我们在把这一方法用于机器视觉和过程控制”。
数学机械化与数学机械化数学是数学的一部分，随着计算机大规模的渗透人们的生活，自然也改变了人们的学习、工作和从事研究的方式，一张纸、一支笔的情景基本上已成为历史。机械化数学的努力就是要将数学的各个领域一部分一部分的机械化，从而使传统数学的许多方面，由于有了数学机械化而面貌一新。这里仅列举一二。
微分几何、代数几何是引人入胜的数学分支，它们不但在理论的发展长河中考验了一大批杰出的数学家，在许多工程应用中也起到了不可替代的作用。Clifford 代数与重要的 E.Cartan外微分运算向结合，形成了局部微分几何定理的机器证明的新算法，利用这一结果可以给出陈省身关于曲面论中一个十分深刻的定理的非常简单的证明。代数几何中，在等价的意义下做分类，是非常重要且基本的问题。在一维情形下，用机械化数学的方法，做出了同构意义下的分类处理，是值得继续扩展成果的方向。
非线性发展方程的解，不仅仅是偏微分方程立论中关心的重要问题，同时它还具有十分明显的物理应用背景，一些著名方程，如力学，固态物理、等离子体物理和化学物理等领域中出现的一类非线性波方程，需要求物理上有兴趣的钟状、纽结状的孤立波解。现在已经应用特征列方法解过几十个非线性波方程，非线性发展方程。所得结果除涵盖已知解外，还发现了许多新解。
相辅相成、互惠互利，是机械化数学与一般数学关系的绝妙写照。
1981年吴文俊在《数学的机械化与机械化的数学》一文中指出：“我们的研究工作还只是一个开端。如何继续发扬中国古代传统数学的机械特色，对数学各个不同领域探索实现机械化的数学，则是本世纪以致可能绵亘整个21 世纪才能大体趋于完善的事。”近 20 年来 ,在吴文俊的积极倡导下，中国的数学机械化研究已初现丰富多彩之势。展望21世纪，我们有理由相信，机械化数学和数学机械化必将为数学以致整个科学注入新的活力。
参考文献
- 吴文俊 . 吴文俊文集 . 济南 : 山东教育出版社 , 1986
- 吴文俊 . 吴文俊论数学机械化 . 济南 : 山东教育出版社 , 1996
- 吴文俊 . 初等几何判定问题与机械化证明 . 中国科学 ,1977,507
- 吴文俊 . 几何定理机器证明的基本原理 ( 初等几何部分 ). 北京 :科学出版社 ,1984
- Wu Wen-tsun. Mathematics Mechanization. Beijing, SciencePress,China & Dordrecht, Kluwer Academic Publishers, TheNetherlands, 2000
- 吴文俊主编 . 王者之路 — 机器证明机器应用 . 长沙 :湖南科学技术出版社 ,1999
- 张景中 . 计算机怎样解几何题 — 谈谈自动推理 . 北京 :清华大学出版社 & 广州 : 暨南大学出版社 ,2000
- 石赫 . 机械化数学引论 . 长沙 : 湖南教育出版社 ,1998
- 程民德主编 . 中国数学发展的若干主攻方向 . 南京 : 江苏教育出版社,1994
- 李继闵 . 《九章算术》及其刘徽注研究 . 西安 : 陕西人民教育出版社,1990
