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

吴文俊数学机械化的成就和意义 自 1976 年冬，中国著名教授吴文俊在中国古代数学机械化思想的启发下，尚不 知外国人的研究成果，独辟蹊径，大胆地投入数学机械化的研究，创建了数学 机械化方法：从几何公理体系出发，引进坐标，将任意几何问题代数化→将证 明题的假设与结论分别表示成多元多项式方程→在电子计算机上运算，以判断 定理是否成立吴文俊教授运用自己的方法，在电子计算机上完成了西姆森线、费尔巴哈 定理、毛莱定理等一系列初等几何的证明随后，他又把证明的范围扩大到非 欧几何、仿射几何、圆几何、线几何、球几何等领域目前，运用吴文俊教授 的方法，已证明出 600 多条定理，许多定理的证明只需几秒甚至零点几秒就可 在电子计算机上完成甚至有一些定理证明相当繁杂，即便交给杰出的数学家 来证，也是相当困难的中国数学家吴文俊，终于实现了千百年来几何定理机械化证明的梦想被 誉为“吴方法”的诞生，给两千多年的公理化演绎体系带来了强烈冲击吴文俊教授还用自己的方法，证明了可以用计算机程序从刻卜勒定律推导 出牛顿定律，这已超出了数学定理机械化证明的范畴，而是属于更广的自动推 理其实，各个科学领域研究的问题，只要涉及到方程求解，“吴方法”都会 有用武之地。

美国《自动推理杂志》编委穆尔认为，“吴方法”建立之前，几何定理机 械化证明的研究处于一片黑暗，吴不仅冲破了这种沉寂的局面，而且带来了光 辉的前景美国自动推理的权威人物淮斯认为，吴文俊在自动推理领域的杰出贡献是 不可磨灭的，他理应获得最高奖吴文俊的心愿：“中国传统数学濒于失传并让位于西方现代数学，已有几 个世纪之久了，现在已到了复兴中国数学事业的紧要关头下个世纪，应该让 中国先哲创立的机械化算法体系在数学领域再领风骚”机械化数学的典范机械化数学的典范————评吴文俊的专著评吴文俊的专著《《几何定理机器证明的基本原理几何定理机器证明的基本原理》》--《《中国科学院院刊中国科学院院刊》》1987 年年 04 期期1899 年希尔伯特(Hilbert)出版了他的经典名著《几何基础》,从此奠定了几何公理化体系的 基础1984 年科学出版社出版的吴文俊的专著《几何定理机器证明的基本原理》(以下简 称《原理》)一书,可以说是奠定了几何机械化体系的基础它可以与《几何基础》媲美,成 为机械化数学的典范著作机器定理证明与数学机械化机器定理证明与数学机械化 1999/12/08 11: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(1899~1980)后文提到的 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) = x1u1–x2u2 = 0 2. D 在 BC 所在直线上，整理得：h2(u1, u2, x1, x2) = x1u2–x2u1–u1u2 = 0条件是 四元二次多项式方程组l 求证代数化：|AD|2 = |CD|·|BD|, 整理得：g1(u1, u2, x1, x2) = 结论 G2: g1(u1, u2, x1, x2) = 0第二步也就是机械化的核心步骤：判断 G2 是否可以由 G1 推出这样的问题就 我们目前所学实在无能为力，甚至说清“推出”二字也很难。

比较明显地我们 说 可以推出 x2–y2–4 = 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}实行这样的除法。