吴文俊数学机械化的成就和意义（精品）

吴文俊数学机械化的成就和意义 自1976年冬，中国著名教授吴文俊在中国古代数学机械化思想的启发下，尚不 知外国人的研究成果，独辟蹊径，大胆地投入数学机械化的研究，创建了数学机 械化方法从几何公理体系出发，引进坐标，将任意几何问题代数化一将证明题 的假设与结论分别表示成多元多项式方程一在电子计算机上运算，以判断定理是 否成立。 吴文俊教授运用自己的方法，在电子计算机上完成了西姆森线、费尔巴哈定 理、毛莱定理等一系列初等几何的证明。随后，他又把证明的范围扩大到非欧几 何、仿射几何、圆几何、线几何、球几何等领域。目前，运用吴文俊教授的方法, 已证明出600多条定理，许多定理的证明只需几秒甚至零点几秒就可在电子计算 机上完成。甚至有一些定理证明相当繁杂，即便交给杰出的数学家来证，也是相 当困难的。 中国数学家吴文俊，终于实现了千百年来几何定理机械化证明的梦想。被誉 为“吴方法”的诞生，给两千多年的公理化演绎体系带来了强烈冲击。 吴文俊教授还用自己的方法，证明了可以用计算机程序从刻卜勒定律推导出 牛顿定律，这已超出了数学定理机械化证明的范畴，而是属于更广的自动推理。 其实，各个科学领域研究的问题，只要涉及到方程求解，“吴方法”都会有用武 之地。 美国自动推理杂志编委穆尔认为，“吴方法”建立之前，几何定理机械 化证明的研究处于一片黑暗，吴不仅冲破了这种沉寂的局面，而且带来了光辉的 前景。 美国自动推理的权威人物淮斯认为，吴文俊在自动推理领域的杰出贡献是不 可磨灭的，他理应获得最高奖。 吴文俊的心愿“中国传统数学濒于失传并让位于西方现代数学，已有几个 世纪之久了，现在已到了复兴中国数学事业的紧要关头。下个世纪，应该让中国 先哲创立的机械化算法体系在数学领域再领风骚”。 机械化数学的典范一一评吴文俊的专著几何定理机器证明的基本原 理“中国科学院院刊1987年04期 1899年希尔伯特（Hilbert）出版了他的经典名著几何基础，从此奠定了几何公理化体系的基 础。1984年科学出版社出版的吴文俊的专著几何定理机器证明的基本原理（以下简称原 理）一书,可以说是奠定了几何机械化体系的基础。它可以与几何基础媲美，成为机械化 数学的典范著作。 机器定理证明与数学机械化 http// 1999/12/08 1100 科技日报 1977年，吴文俊证明初等几何主要一类定理的证明可以机械化（即刻板化、 程序化、算法化）。1978年，吴文俊又证明初等微分几何中的一些主要定理的 证明也可以机械化。其后，他把机器定理证明的范围推广到非欧几何、仿射几何、 圆几何、线几何、球几何等领域。 继机器定理证明之后，吴文俊把研究重点转移到数学机械化的核心问题 方程求解上来，得出了作为机械化数学基础的整序原理及零点结构原理， 它不仅可用于代数方程组，还可以解代数偏微分方程组，从而大大扩充了理论及 应用的范围。国际上公认的“吴方法”不仅在机器定理证明、代数系统求解的理 论和算法上，而且在物理学、化学、计算机科学、数学科学和机器人机构学等方 面的应用上都取得了国际领先成果。 吴文俊是从对中国传统数学的机械化特征进行深入分析后得出数学机械化 的思想和方法的。他的目标是在数学的各个领域全面推行机械化。这一宏伟纲领 是继承中国传统文化精华和实现中华民族伟大复兴在数学领域的正确途径。 把数学的整类定理（数量可很多甚至无穷尽）整体地考虑，建立统一、确定的证明程序，机 械地、按部就班地逐步实施，经有限步即可推断数学命题的真假（真者即为定理），称为数 学定理的机械化证明。世界著名数学家、中国科学院院士吴文俊运用以他姓氏命名的“吴氏 原理”，在国际上首次实现大量相当困难的数学定理的机械化证明；1997年，在中国科学 发表划时代论文初等几何判定问题与机械化问题；1978年，在微分几何定理的机械化工 作方面获突破；1984年，出版极为重要的几何定理机器证明的基本原理；1995年，出版 专著吴文俊论数学机械论。著名数学家张景中院士和杨路教授等人则另辟蹊径，开发数 学教育软件，从非线性代数方程组的机器证明入手，发展计算机自动推理，实现了不等式乃 至更广泛的数学形式的机器证明，取得国际瞩目的成就。吴文俊荣获首届国家自然科学最高 奖，奖金500万元人民币。中国数学机械化学派已处于世界领先地位，正朝着更深入、更全 面的各个数学领域的机械证明的宏伟前景进军。 几何定理的机器证明时间2010-03-26 2050来源网络 作者佚名 点击234次 讲述了用计算机自动证明某一类型几何定理，甚至某一种几何全部定理的原理和 方法。 现在大家应该已经形成这样的认识算法就是针对一类问题的程序性方法，所谓 程序性就是每前进一步都有章可循地确定下一步做什么和怎么做。从思想方法上 你一定感到这与我们学过的欧氏几何有很大不同，算法思想是从问题解决出发给 出算法解而不是按照定义一公理一定理一证明的演绎系统进行的，此二者 就是数学发展史中发挥巨大作用的机械化思想和公理化思想。 与源于古希腊的欧氏几何不同，中国古代的几何学乃至整个数学是“术”（算法） 的科学，强调构造性、算法化，注意解决科学实验和生产实践中提出的各类问题。 例如由观天测地产生的勾股弦公式、日高公式等都是这样的，又如在四元玉鉴 中己经指出，如果引入天元（即未知数）并建立相应的方程，通过解方程即可自然 导出这些几何公式。由此提供了一条证明与发现几何定理的新路把非机械化的 定理求证归结为机械化的方程求解。首届（2001年）国家最高科技奖获得者吴 文俊先生曾明确提出，中国古代数学是一种机械化数学，数学机械化思想是中国 古代数学的精髓。吴先生的研究起到了正本清源的作用，证实中国古代数学是世 界数学的主流之一，促进了西方数学与中国古代数学两大主流的融合，推动了数 学的发展，同时也掀起了对中国数学史再认识的新高潮。 吴文俊 公理化体系的几何定理证明非常不机械化。我们都有这样的经验，一个平面几何 定理的证明，往往要经过冥思苦想，奇巧构思，无章可循地添加辅助线，迂回曲 拆地给出证明。如何利用计算机进行自动推理,特别是进行几何定理的自动证明， 是学术界长期研究的课题。所谓定理的机械化证明，就是对一类定理这类定理 可能成千上万提供一种统一的算法，使得该类定理中每个定理，都可依此方法 给出证明。从“一理一证”到“一类一证”，这是数学认识和实践的飞跃。 我们研究的几何机械化问题历史上可以追溯至十二、三世纪宋元时期初次出现的 几何学代数化，将几何学问题化为多项式问题，以及相伴而生的多项式组消去法。 事实上，早在17世纪大哲学家、大思想家和大数学家莱布尼兹就有机械化证明 的设想。只是直到19世纪末及以后由于希尔伯特及其追随者们建立并发展了数 理逻辑，这一问题才具有了明确的数学形式。又由于20世纪40年代计算机的出 现，才使这一设想有了现实的意义。以下我们按照时间顺序简要介绍一下几何机 械化的背景 在希尔伯特的经典著作几何基础中我们可以发现两条机械化定理H和P,这 一类可机械化的几何定理的特征是假设部分的代数关系