吴文俊数学机械化的成就和意义.doc

吴文俊数学机械化的成就和意义自1976年冬，中国著名教授吴文俊在中国古代数学机械化思想的启发下，尚不知外国人的研究成果，独辟蹊径，大胆地投入数学机械化的研究，创建了数学机械化方法：从几何公理体系出发，引进坐标，将任意几何问题代数化将证明题的假设与结论分别表示成多元多项式方程在电子计算机上运算，以判断定理是否成立。 吴文俊教授运用自己的方法，在电子计算机上完成了西姆森线、费尔巴哈定理、毛莱定理等一系列初等几何的证明。随后，他又把证明的范围扩大到非欧几何、仿射几何、圆几何、线几何、球几何等领域。目前，运用吴文俊教授的方法，已证明出600多条定理，许多定理的证明只需几秒甚至零点几秒就可在电子计算机上完成。甚至有一些定理证明相当繁杂，即便交给杰出的数学家来证，也是相当困难的。 中国数学家吴文俊，终于实现了千百年来几何定理机械化证明的梦想。被誉为“吴方法”的诞生，给两千多年的公理化演绎体系带来了强烈冲击。 吴文俊教授还用自己的方法，证明了可以用计算机程序从刻卜勒定律推导出牛顿定律，这已超出了数学定理机械化证明的范畴，而是属于更广的自动推理。其实，各个科学领域研究的问题，只要涉及到方程求解，“吴方法”都会有用武之地。 美国自动推理杂志编委穆尔认为，“吴方法”建立之前，几何定理机械化证明的研究处于一片黑暗，吴不仅冲破了这种沉寂的局面，而且带来了光辉的前景。 美国自动推理的权威人物淮斯认为，吴文俊在自动推理领域的杰出贡献是不可磨灭的，他理应获得最高奖。 吴文俊的心愿：“中国传统数学濒于失传并让位于西方现代数学，已有几个世纪之久了，现在已到了复兴中国数学事业的紧要关头。下个世纪，应该让中国先哲创立的机械化算法体系在数学领域再领风骚”。 机械化数学的典范评吴文俊的专著几何定理机器证明的基本原理-中国科学院院刊1987年04期1899年希尔伯特(Hilbert)出版了他的经典名著几何基础,从此奠定了几何公理化体系的基础。1984年科学出版社出版的吴文俊的专著几何定理机器证明的基本原理(以下简称原理)一书,可以说是奠定了几何机械化体系的基础。它可以与几何基础媲美,成为机械化数学的典范著作。机器定理证明与数学机械化 1999/12/0811:00 科技日报1977年，吴文俊证明初等几何主要一类定理的证明可以机械化（即刻板化、程序化、算法化）。1978年，吴文俊又证明初等微分几何中的一些主要定理的证明也可以机械化。其后，他把机器定理证明的范围推广到非欧几何、仿射几何、圆几何、线几何、球几何等领域。继机器定理证明之后，吴文俊把研究重点转移到数学机械化的核心问题方程求解上来，得出了作为机械化数学基础的整序原理及零点结构原理，它不仅可用于代数方程组，还可以解代数偏微分方程组，从而大大扩充了理论及应用的范围。国际上公认的“吴方法”不仅在机器定理证明、代数系统求解的理论和算法上，而且在物理学、化学、计算机科学、数学科学和机器人机构学等方面的应用上都取得了国际领先成果。吴文俊是从对中国传统数学的机械化特征进行深入分析后得出数学机械化的思想和方法的。他的目标是在数学的各个领域全面推行机械化。这一宏伟纲领是继承中国传统文化精华和实现中华民族伟大复兴在数学领域的正确途径。把数学的整类定理（数量可很多甚至无穷尽）整体地考虑，建立统一、确定的证明程序，机械地、按部就班地逐步实施，经有限步即可推断数学命题的真假（真者即为定理），称为数学定理的机械化证明。世界著名数学家、中国科学院院士吴文俊运用以他姓氏命名的“吴氏原理”，在国际上首次实现大量相当困难的数学定理的机械化证明；1997年，在中国科学发表划时代论文初等几何判定问题与机械化问题；1978年，在微分几何定理的机械化工作方面获突破；1984年，出版极为重要的几何定理机器证明的基本原理；1995年，出版专著吴文俊论数学机械论。著名数学家张景中院士和杨路教授等人则另辟蹊径，开发数学教育软件，从非线性代数方程组的机器证明入手，发展计算机自动推理，实现了不等式乃至更广泛的数学形式的机器证明，取得国际瞩目的成就。吴文俊荣获首届国家自然科学最高奖，奖金500万元人民币。中国数学机械化学派已处于世界领先地位，正朝着更深入、更全面的各个数学领域的机械证明的宏伟前景进军。几何定理的机器证明时间:2010-03-26 20:50来源:网络 作者:佚名 点击:234次 讲述了用计算机自动证明某一类型几何定理，甚至某一种几何全部定理的原理和方法。现在大家应该已经形成这样的认识：算法就是针对一类问题的程序性方法，所谓程序性就是每前进一步都有章可循地确定下一步做什么和怎么做。从思想方法上你一定感到这与我们学过的欧氏几何有很大不同，算法思想是从问题解决出发给出算法解而不是按照定义公理定理证明的演绎系统进行的，此二者就是数学发展史中发挥巨大作用的机械化思想和公理化思想。与源于古希腊的欧氏几何不同，中国古代的几何学乃至整个数学是“术”（算法）的科学，强调构造性、算法化，注意解决科学实验和生产实践中提出的各类问题。例如由观天测地产生的勾股弦公式、日高公式等都是这样的，又如在四元玉鉴中己经指出，如果引入天元(即未知数)并建立相应的方程，通过解方程即可自然导出这些几何公式。由此提供了一条证明与发现几何定理的新路：把非机械化的定理求证归结为机械化的方程求解。首届（2001年）国家最高科技奖获得者吴文俊先生曾明确提出，中国古代数学是一种机械化数学，数学机械化思想是中国古代数学的精髓。吴先生的研究起到了正本清源的作用，证实中国古代数学是世界数学的主流之一，促进了西方数学与中国古代数学两大主流的融合，推动了数学的发展，同时也掀起了对中国数学史再认识的新高潮。吴文俊公理化体系的几何定理证明非常不机械化。我们都有这样的经验，一个平面几何定理的证明，往往要经过冥思苦想，奇巧构思，无章可循地添加辅助线，迂回曲拆地给出证明。如何利用计算机进行自动推理，特别是进行几何定理的自动证明，是学术界长期研究的课题。所谓定理的机械化证明，就是对一类定理（这类定理可能成千上万）提供一种统一的算法，使得该类定理中每个定理，都可依此方法给出证明。从“一理一证”到“一类一证”，这是数学认识和实践的飞跃。我们研究的几何机械化问题历史上可以追溯至十二、三世纪宋元时期初次出现的几何学代数化，将几何学问题化为多项式问题，以及相伴而生的多项式组消去法。事实上，早在17世纪大哲学家、大思想家和大数学家莱布尼兹就有机械化证明的设想。只是直到19世纪末及以后由于希尔伯特及其追随者们建立并发展了数理逻辑，这一问题才具有了明确的数学形式。又由于20世纪40年代计算机的出现，才使这一设想有了现实的意义。以下我们按照时间顺序简要介绍一下几何机械化的背景：在希尔伯特的经典著作几何基础中我们可以发现两条机械化定理H和P，这一类可机械化的几何定理的特征是假设部分的代数关系式对于某些特定变量都必须是线性的。这种机械化方法效率最高，即使用手算也可证明颇不简单的定理，但其使用范围过于狭窄。20世纪30年代，美国数学家J.F.Ritt提出了代数几何的构造性理论，并首先提出了多项式组约化整序、特征列等概念，为吴文俊后来的工作铺平了道路。一个必须介绍的人物是波兰数学家Tarski，他在1948的一篇经典著作中解决了实闭域的判定问题，其主要目的之一是给出初等几何定理的机械化证明。只是该方法效率颇低，虽经Seidenberg等人优化仍是繁到不可收拾，因而远远不是切实可行的。1964年Hironaka提出了Grobner基的概念，他称之为“标准基”。1965年B.Buchberger在他的博士论文中深入研究了Grobner基的性质，并给出了Grobner基的算法及改进算法，Grobner基的名称来自于Buchberger的导师W.Grobner(18991980)。后文提到的Grobner基方法就是源于对Grobner基性质和算法的应用。吴方法是20世纪70年代末吴文俊先生受中国古代数学机械化思想影响，借助30年代Ritt的理论工作，针对几何定理机器证明问题研究和发展的新方法。吴先生不仅作了许多理论工作，鉴于吴方法的高效性，他还进行了大量的机证实验，证明和发明了不少几何定理。他的工作也影响了国内外一大批数学工作者，将几何机械化乃至整个数学的进程向前推进了一大步。适用吴方法证明的定理有下面特征：假设与结论部分的代数关系式都可以用多项式方程来表示。具体地说：设A,B,C,D,E,F是平面上的点，借助解析几何知识下列几何性质可以表达为一个或几个多项式方程：AB平行于CD； AB垂直于CD； A,B,C共线； AB=CD； C在以A为原点，AB为半径的圆上； C是AB中点； 锐角ABC与锐角DEF相等； BD是角ABC的平分线。 一般地，几何定理机器证明问题可以分成下面两个主要步骤：第一步，用解析几何方法建立坐标系设未知量，将条件表示成所设未知量的多项式方程组G1，将求证表示成多项式方程组G2.（几何的代数化与坐标化） 第二步，用一定算法（如吴方法）判断G2是否可以由G1推出。（代数讨论的机械化） 我们也分这两步来介绍。第一步只要看一个简单的例子：射影定理的代数化求证：直角三角形斜边上的高是斜边两线段的比例中项。建立坐标系、设未知量如图：l 条件代数化：1. AD垂直于BC，斜率互为负倒数，整理得：h1(u1, u2, x1, x2) = x1u1x2u2 = 02. D在BC所在直线上，整理得：h2(u1, u2, x1, x2) = x1u2x2u1u1u2 = 0条件是 四元二次多项式方程组l 求证代数化：|AD|2 = |CD|BD|, 整理得：g1(u1, u2, x1, x2) = 结论G2: g1(u1, u2, x1, x2) = 0第二步也就是机械化的核心步骤：判断G2是否可以由G1推出。这样的问题就我们目前所学实在无能为力，甚至说清“推出”二字也很难。比较明显地我们说 可以推出x2y24 = 0还可以推出x = 0等，但是对多元高次的多项式方程组我们就必须借助高等的数学工具和计算机算法来帮忙了。一种可行的算法是借助前面提过的Grobner基的性质，用计算机去求由多项式组hi和g生成的一种代数结构的Grobner基（一组多项式），看这组基中是否包含数字1来判断是否可以推出结论g = 0. 吴方法同样是由hi构造一组多项式，称为广义特征列。判断g = 0对广义特征列的拟除余式是否为0，就知道求证是否成立了。上述算法很难理解，事实上多项式方程组求解的问题非常困难，对这个问题的探索理论上引发了代数几何学的建立。我们试着用简单的语言对上面的方法作一点解说：（解释原理，数学上不一定精确）要证多项式方程g = 0由多项式方程组hi = 0推出，就是要证：g = c1h1 + c2h2 + cnhn, 其中ci是和g, hi含有相同变元的多项式组。一种朴素的想法是g关于hi做除法：用h1去除g, 再用h2去除余式m1, 再用h3去除余式m2只要最后hn除余式mn-1为0即可。但是由射影定理的例子可见g关于hi实行这样的除法是行不通的。于是我们想办法转化：Grobner基与广义特征列都是多项式组pi，使得所有写成d1p1 + d2p2 + dmpm形式的多项式的0点集合就是所有c1h1 + c2h2 + cnhn形式多项式的0点集合（这个集合是令多项式为0的各变元取值的集合，几何上称仿射簇，可以理解为保证多项式方程组同解）。于是问题转化成证明g = d1p1 + d2p2 + dmpm，由于Grobner基与广义特征列具有很好的代数性质，两种算法都可以采用类似多项式除法的办法进行验证。Gröbner基方法中考虑g模pi约化的范式（类似于前述多项式除法的最终余式），范式为0说明g = 0 可由pi = 0推出，定理得证。吴方法中考虑g关于pi拟除的余式Rem(g, pi), 余式为0定理得证。需要指出的是求Grobner基与广义特征列的过程同时也是多项式方程组消元的过程，比证明g = 0用途更广泛的是这两种方法同时给出了求解多项式方程组的有效算法（即使不能求出每个未知量，至少可以保证同解地消掉其中的一部分变元，因而也可用于多参数方程组消参），宏观上这类似前面正文讨论的消元法，因此吴方法也被称为吴消元法。同时吴文俊先生大力倡导数学机械化的应用，如应用于线性控制系统、机构综合设计、平面星体运行的中心构形、化学反应方程的平衡、代数曲面的光滑拼接、从开普勒定律自动惟出牛顿定律、全局优化求解等等。在他的指导和带动下，数学机械化方法还在一些交叉研究领域