几何定理机器证明的方法——吴方法思想的形成，本文主要内容关键词为：定理论文,几何论文,机器论文,思想论文,方法论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
计算机在自己发展的早期就与数学结下了不解之缘.众所周知，数值计算无论是在数学发展之初，还是现在，甚至在未来的数学发展中都将占据着至关重要的地位.因此，在解决越来越复杂的数值计算过程中，世界各民族都创造了各式各样的计算工具：屈指计算→卵石计算（结绳计算、刻痕计算）→算筹→算盘→计算尺→……，而计算机成了数值计算工具中的佼佼者，从手摇（机械）计算机→电动（机械）计算机→直到现在发展的高速电子计算机（电脑）.计算机作为数值计算工具的发明要归功于15世纪法国著名的数学家、物理学家和思想家帕斯卡（B.Pascal，1623～1662）.帕斯卡的“加法机”是计算工具史上的一个里程碑，因为它包含着后来计算机的基本原理，为后来机械计算机的制造迈出了开拓性的一步.他自己在《沉思录》中也认为，计算器所进行的工作，比动物的行为，更接近人类的思维.法国天文学家、数学家华纳在评论帕斯卡计算机的设计思想时，曾说过，“帕斯卡的思想，特别是在当时，可以算作是非凡的勇敢.因此他提出了这样的目的，即利用纯粹机械装置，来代替我们的思考和记忆.”毫无疑问，这种非凡的思想为后人提出用机器来执行推理，以至用机器执行几何定理证明给以极大的启发.
帕斯卡之后，人们又相继制造出了进行加减运算、乘法运算和开方运算的机器.尽管这些机器为简化当时人们的计算提供了极大的便利，然而所存在的缺陷使得它们无法适应社会发展对计算提出的要求，所以最终没有得到推广.不过他们的思想却被后人继承下来，特别是随着科学、技术的进步和物质条件的日益成熟，计算机获得了更加长足的发展.1976年12月《科学》杂志上发表了当代计算机科学大师克努思（D.Knuth）的一篇文章，就描述了计算机强大的计算能力，“把10位数字和10位数字相加，如果用笔算的话，每次约需0.2秒钟.如果采用中型计算机来算这样的加法的话，每秒钟可以进行200，000次，而如果采用快速计算机的话，则每秒钟可达200，000，000次.换句话说，一台中型计算机，就能把人的计算能力提高到6个数量级.克努思说，计算机的计算速度和人的笔算速度比起来，就好比是最快的飞机和蜗牛爬行的速度相比.”（注：吉纳.B.库腊塔：《计算机进入到数学研究领域，数学的优美结束了》，《世界科学译刊》，1979年第1期.）进入21世纪后，计算机的计算速度更是大得惊人，正是这种惊人的高速度，使得计算机对数学的影响远远地超出了其最初作为计算的功能，成为几何定理机器证明的工具.
明确提出机器可成为推理工具的思想，要追溯到17世纪德国著名的数理逻辑学家、哲学家和微积分的创始人之一莱布尼茨（G.W.Leibniz，1646～1716）.莱布尼茨想必受到帕斯卡“这种计算器所进行的工作，比动物的行为，更接近人类的思维”的重要思想（注：为了制造计算机，他从德国移居到法国.）和笛卡儿（1596～1650）解析几何思想的启发，想到可以创造一种通用的语言，以实现推理的机械化，从而把很多问题的处理机械化.笛卡儿创立解析几何，目的是将几何的推理过程归结为代数的计算问题.根据帕斯卡所设计的机器，是可以将代数的计算问题机械化的.因此，莱布尼茨想建立一种演算，根据这种演算，可将推理转化为计算，遇到争论，双方只要把笔拿在手里说，“让我们来计算一下吧”，所有的问题者可迎刃而解.
遗憾的是，由于所处时代的限制，莱布尼茨没有实现他的梦想，但他的思想却被后人发展了，特别是促进了布尔代数、数理逻辑的研究，而这为我们今日实现定理证明机械化提供了理论基础；而得益于布尔代数、数理逻辑成就的计算机科学的发展，又为我们实现定理证明机械化提供了物质基础.
定理证明作为数学研究中的一项重要工作，向来受到人们的关注.尤其是在中学，它还被视为训练逻辑思维的绝好素材.众所周知，为了完成一个定理的证明，有时要花费一个人或者是几个人一辈子、或者是几辈子的时间.即使如此，有时候也还是找不到合适的证明，像大家熟悉的四色定理.正是由于定理证明的艰难，才使得在数学历史上几代人有一个共同的梦：把定理证明特别是几何定理的证明机械化.20世纪之前，只有笛卡儿的解析几何在一定程度上为几何定理的证明从质的困难转化为量的困难提供了可行的方法.可是由于当时物质条件的限制，还不得不停留在手工操作上.当然，用机器实现几何定理证明甚至是推理的机械化的想法并不为所有的人接受.著名的法国数学家庞加莱（J.H.Poincare，1854～1912）就曾对这一想法大加责难，还形象地讥讽说，现在已经有屠宰机，当把牲畜赶到机器的一端时，机器便把这些牲畜宰杀成罐头，从另一端输送出来；现在有人竟然想制造一部机器，当把定理的条件送到机器的一端后，便可以把定理的结论从机器的另一端输送出来（或者公理、定义送到一端后，各式各样的定理便从另一端输送出来），这种想法注定是不可能实现的.
尽管有一代大师的否定预言，可是20世纪二、三十年代以来计算机的快速发展，使得一些数理逻辑学家们又开始探讨定理证明机械化的可能性.Herbrand 1930年从数理逻辑角度奠定了定理机器证明的理论基础，最终为人工智能的开发提供了条件.波兰数学家、数理逻辑学家塔斯基（1902～1983）在1950年得到一个引人注目的结论：一切初等几何和初等代数范围的命题，都可以用机械方法判定，并开拓了用代数方法解决机器证明的方向.但是由于他的判定方法太复杂，以致到现在实践中仍然没有取得太大的进展；1959年，美籍数理逻辑学家、洛克菲勒大学教授王浩（1921～1999）在这方面做出了鼓舞人心的工作：他在计算机上只用了9分钟就证明了罗素（B.A.W.Russell 1872～1970）和怀特海（A.N.Whitehead，1861～1947）所著《数学原理》中的350多个命题，并第一次明确地提出了“走向数学的机械化”的口号.
计算机技术的发展并没有让人们顺利地在几何定理证明领域中取得成就，相反由于没有取得什么较多成果而又让一些人对机器定理证明产生了消极态度.谁知柳岸花明又一村，1983年在美国科罗拉多州举行的全美定理机器证明的学术会议上，大陆赴美求学的青年学者周咸青的报告“Proving elementary geometry theorem using Wu’s Algorithm”，为自动推理领域中的专家学者带来了意外的惊喜：他可以在计算机上自动地证明几百条困难的几何定理，而且一条定理证明只需要几秒钟.而他所运用的方法就是中国著名数学家吴文俊教授建立和发展的机器证明代数消元法.
吴文俊教授20世纪70年代之前的主要工作是在代数拓扑学上，并在这一领域做出了一系列基本的、意义深远的开创性工作.在20世纪70年代之后，他在继续代数拓扑学领域研究的同时，开始钻研中国古代数学，为研究中国古代数学史开创了一个新阶段，并提出了数学史研究的科学方法（注：在第20届国际数学家大会上提炼为两条原则：一、所有研究结论应该在幸存至今的原著的基础上得出；二、所有结论应该利用古人当时的知识、辅助工具和惯用的推理方法得出.），因此强有力地批驳了国外许多数学史家言必称希腊的错误，“被颠倒了的历史必须被颠倒过来！”（注：《中国古代数学对世界文化的伟大贡献》，《数学学报》，1975年第18期.）.通过对中国古代数学的研究，他发现中国古代数学实质上是与古代希腊数学相平行的两条发展路线之一.不仅如此，吴先生通过对中国古代数学史的研究，还树立了古为今用的新典范——开辟了数学机械化的新时代.
“我们从事机械化定理证明工作获得成果之前，对泰斯基的已有工作并无接触，更没有想到希尔伯特的《几何基础》会与机械化有任何关系.”（注：《数学的机械化》，《百科知识》，1980年.）“至于Tarski与Hilbert，则虽然他们的工作是一般数学家大体上都知道的，但真正和我的几何定理机器证明与数学机械化联系起来，则是在我几何定理机器证明取得成功（时在1976、77年之交）以后的事.
80年代我在研究生院为博士生开设数学机械化的课程，把Hilbert的几何基础一书作为参考读物.在教学过程中发现书中的一条定理，可以解释为某种特殊类型几何定理的机械化证明，为此我写了两篇短文，并把Hilbert的这一定理称之为Hilbert机械化定理，那已是1984年的事了.”（注：引自吴文俊先生给笔者的信.）“本书所阐述的几何定理证明的机械化问题，从思维到方法，至少在宋元时代就有蛛丝马迹可寻.虽然这是极其原始的，但是，仅就著者本人而言，主要是受中国古代数学的启发.”（注：吴文俊：《几何定理机器证明的基本原理》（初等几何部分），科学出版社，1984年版.）吴文俊先生是如何将几何定理的机器证明与中国古代传统数学联系起来呢？
“中国的数学家，除了专门从事中国古代数学史的专家们以外，绝大多数的中国数学家，包括陈省身先生和我，由于所受教育以及西方史书的影响，对中国的古代数学都是比较轻视认为不足道的.
我自己的转变源于1974年数学所号召全所学习中国古代数学.我这时才真正学习中国古代数学，懂得了其丰富而深刻的内容，西方史书所说有许多不实之处，这决定了我此后对数学的新的认识与新的研究道路.”（注：引自吴文俊先生给笔者的信.）
“欧几里得传统是公理化、演绎推理与证定理.中国传统数学则着重解决具体问题，从问题出发，由此自然导致方程求解.Descartes的几何学一书是与中国的传统数学精神相符的.我从事几何定理证明时，首先选取适当坐标，于是几何定理的假设与终结通常都成为多项式方程，称之为假设方程组与终结方程.满足定理假设的几何图象，就相当于假设方程组的一个解答或零点.要证明定理成立，就是要证明这样的零点也使终结多项式为0.中国的传统数学主要是解方程（而不是证定理），它提供了解任意多项式方程组的方法，因之提供了求得所有假设方程组的解答或零点的方法，由此解答就可检查这些零点是否也是终结方程的解答或零点，也就提供了证明几何定理的方法.换言之，几何定理的证明可以看作是中国传统数学解方程的一个具体应用.”事实上，通过对中国古代数学的研究，吴先生发现我们先人解决问题的思路可以用“机械化”一词加以概括.因为“四则运算与开平方的机械化算法由来已久.汉初完成的《九章算术》中，对开平方、开立方的机械化过程，就有详细说明，到宋代更发展到高次代数方程求数值解的机械化算法.……在宋元时代，我国就创立了‘天元术’，引进了天元，以及地元、人元、物元等相当于现代未知数的概念，把相当多的问题特别是几何问题转化为代数方程与方程组的求解问题.这一方法用于几何可称为几何的代数化.12世纪的刘益将新法与‘古法’比较，称‘省功数倍’.与之相伴而生，又引进了相当于现代多项式的概念，建立了多项式的运算法则和消元法的有关代数工具，使几何代数化的方法得到了有系统的发展，具见于宋元时代幸以保存至今的杨辉、李冶、朱世杰的许多著作中.”（注：《数学的机械化》，《百科知识》，1980年第？期.）
古代中国数学研究的核心是问题求解，这从中国最早的代表作《九章算术》可就可以看到，而问题的解决最终无不是转化为方程或者方程组的求解.运用开平方法、增乘开平方法等方法，我们的先人获得了许多方程的求解，而宋元时期的朱世杰在《四元玉鉴》中所发明的“四元术”（注：所谓四元，是“…按天、地、人、物，立成四元”，而四元术是指“四元高次方程组的布列和解法”.引自《中国数学简史》，中外数学简史编写组，山东教育出版社，1986年版，第332页.），则使解高次方程组特别是四元高次方程组的方法达到了相当高的水平.然而由于当时是用算筹作为计算工具，所以未知数的个数只能限于四个（因为解方程组时需要将各不同类型项的系数（用算筹表示）布置在算盘的特定位置上，所以未知数的个数太多时，会因计算量太大而很难完成）.事实上，若改用纸笔运算，则4个未知数的限制完全可以打破，而四元术中的原理与方法，依然可适用于解任意多个未知数的高次联立方程组.考察四元术的运用，可以发现它的一个重要思想是消元，而这种消元又是可以机械地执行.吴先生所创立的“吴方法”，正是鉴戒了中国古代数学中解方程组的思想，尤其是朱世杰四元术中的可机械执行的消法思想.
在几何定理的机器证明上，吴方法与以前许多方法相比较都要优越得多，例如“在电子计算机出现后不久，一位专家曾经估计：一个有26个未知数的联立方程组，在电子计算机上用18世纪在欧洲出现的“克莱默方法”来解，得花十万万万万年；如果用消去法来解，只要用3秒钟就够了.”（注：《吴文俊论数学机械化》，山东教育出版社，1996年版第25页.）
关于吴方法在技术上与中国古代数学尤其是与朱世杰的四元术之间是如何建立联系的，在以后的文章中再作进一步的探讨.
（感谢吴文俊先生在百忙中为我写信陈述有关问题，也感谢董光璧先生对我的指导.）