人机大战与机器证明

1、享誉世界的“吴方法”几何定理的机器证明2001年2月19日，中华人民共和国国家科学技术奖颁奖大会在北京人民大 会堂隆重举行，国家主席江泽民亲自为荣获国家科学技术奖的科学家发奖。荣 获这一届国家科学技术奖的两位著名科学家之一就是吴文俊。他是因为在几何 定理的机器证明方面的科研成果而获该年度国家科学技术奖的。计算机作为数值计算工具的发明要归功于十五世纪法国著名数学家、物理 学家和思想家帕斯卡。帕斯卡在 1644年制造的“加法机”是计算工具史上的一个 里程碑，因为它包含着后来计算机的基本原理，为后来机械计算机的制造迈出 了开拓性的一步。他自己在沉思录中也认为，计算器所进行的工作，比动 物的行为，更接

2、近人类的思维。法国天文学家、数学家华纳在评论帕斯卡计算 机的设计思想时，曾说过，“帕斯卡的思想，特别是在当时，可以算作是非凡的 勇敢。因为他提出了这样的目的，即利用纯粹机械装置，来代替我们的思考和 记忆。”毫无疑问，这种非凡的思想为后人提出用机器来执行推理，以至用机器 执行几何定理证明以极大的启发。帕斯卡以后，人们又相继制造了进行加减运算，乘法运算和开方运算的机 器，但是，所存在的缺陷使得它们无法适应社会发展对计算提出的要求，所以 最终没有得到推广，不过他们的思想却被后人继承下来。进入二十一世纪后， 计算机的计算速度更是大得惊人，正是这种惊人的高速度，使得计算机对数学 的影响远远超出了其最初作

3、为计算工具的功能， 成为几何定理机器证明的工具最初是十七世纪德国数理逻辑学家、哲学家和微积分的创始人之一的莱布 尼兹，明确提出机器可以成为推理工具的思想，他可能是受到帕斯卡的思想和 笛卡尔解析几何思想的启发，想到可以创造一种通用的语言，以实现推理的机 械化，从而把很多数学问题的处理机械化。为了将几何的推理过程归结为代数 的计算问题，笛卡尔创立了解析几何，帕斯卡设计的机器，可以将代数的计算 问题机械化，因此，莱布尼兹想建立一种演算，可以将推理转化为计算。遗憾 的是，由于所处时代的限制，莱布尼兹没有实现他的梦想，但是他的思想却被 后人发展了。定理证明历来受到人们的关注，为了完成一个定理证明，有时要

4、花费一个 人或几个人一辈子或几辈子的时间，即使如此，有时也还是找不到合适的证明 正由于定理证明的艰难，才使得在数学历史上几代人有一个共同的梦想：把定 理证明特别是几何定理证明机械化。当然，用机器实现几何定理证明无论在理论上还是在实践上都不可能是一 帆风顺的。首先，用机器实现几何定理的证明甚至是推理的机械化的想法并不 为所有的人接受。著名的法国数学家庞加莱就曾对这一想法大加责难，认为这 种想法注定是不可能实现的。后来虽然从数理逻辑角度奠定了定理机器证明的 理论基础，并得到引人注目的结论：一切初等几何和初等代数范围的命题，都 可以用机械方法判定。以及1959年美籍数理逻辑学家王浩在这方面做出了鼓舞

5、 人心的工作，但是，计算机技术的发展并没有让人们顺利地在几何定理证明领 域中取得成就，这又让一些人对机器定理证明产生了消极态度。柳暗花明又一村，1983年在美国科罗拉多州举行的全美定理机器证明学术 会议上，大陆赴美求学的青年学者周咸青的报告，为自动推理领域的专家学者 带来了意外的惊喜：他可以在计算机上自动地证明几百条困难的几何定理，而 且一条定理证明只需几秒钟。他所运用的方法就是中国著名数学家吴文俊教授 建立和发展的机器证明代数消元法一一吴方法。“吴方法”是受中国古代数学思想的影响而产生的。吴文俊教授通过对中国古 代数学的研究，发现我们先人解决问题的思路可以用“机械化”一词加以概括。因 为“四

6、则运算与开平方的机械化算法由来已久。汉初完成的九章算术中，对 开平方、开立方的机械化过程，就有详细说明，到宋代更发展到高次代数方程 求数值解的机械化算法。在宋元时代，我国就创立了天元术，引进了天元、地 元、人元、物元等相当于现代未知数的概念，把相当多的问题特别是几何问题 转化为代数方程与方程组的求解问题。这一方法用于几何可称为几何的代数化。 十二世纪的刘益将新法与古法比较，称省功数倍与之相伴而生，又引进了相 当于多项式的概念，建立了多项式的运算法则和消元法的有关代数工具，具见 于宋元时代幸以保存至今的杨辉、李冶、朱世杰的许多著作中。”吴文俊教授所创立的“吴方法”正是鉴戒了中国古代数学中解方程组

7、的思想，几何定理的机器证 明可以看作是中国传统数学解方程的一个具体应用“欧几里得传统是公理化、演绎推理与证定理。中国传统数学则是着重解决 具体问题，从问题出发，由此自然导致方程求解。”我从事几何定理证明时，首 先选取适当坐标，于是几何定理的假设与终结通常都成为多项式方程，称之为 假设方程组与终结方程。满足定理假设的几何图象，就相当于假设方程的一个 解答或零点。要证明定理成立，就是要证明这样的零点也使终结多项式为 00中 国传统数学主要是解方程（而不是证定理），它提供了解任意多项式方程组的方 法，因之提供了求得所有假设方程组的解答或零点的方法，由此解答就可检查 这些零点是否也是终结方程的解答或零

8、点，也就提供了证明几何定理的方法。（数学通报2003年第6期第6页）在几何定理的机器证明上，吴方法与以前许多方法相比较都要优越得多【附录】、【吴文俊简介】吴文俊，男，1919年5月出生于上海，1940年毕业于上 海交通大学数学系。1979年至现在任中国科学院系统科学研究 所副所长、名誉所长、研究员。吴文俊院士是著名的数学家，他的研究工作涉及到数学的诸多领域。在多 年的研究中取得了丰硕成果。其主要成就表现在拓扑学和数学机械化两个领 域。他为拓扑学做了奠基性的工作。他的示性类和示嵌类研究被国际数学界称 为吴公式”吴示性类”吴示嵌类”至今仍被国际同行广泛引用，影响深远, 享誉世界二十世纪70年代后期

9、，在计算机技术大发展的背景下， 他继承和发展了中国古代数学的传统（即算法化思想），转而研究几何定理的机器证明，彻底改变 了这个领域的面貌，是国际自动推理界先驱性的工作，被称为吴方法”产生了巨大影响。吴文俊的研究取得了一系列国际领先成果并已应用于国际上当前 流行的符号计算软件方面。在50多年的研究工作中，吴文俊始终站在数学领域的前沿，做出了原创性 研究成果。在国际上产生了重大影响。二、【菲尔兹奖简介】菲尔兹奖是国际上为奖励在数学研究中作出多方面重大贡献的数学家而设置的。菲尔兹奖从1936年第十届国际数学家会议开始授予以来，截止2002年,共有44位菲尔兹奖得主，它对数学的发展起了不可估量的作用。

10、这个奖的发起人菲尔兹是加拿大数学家，他在代数函数方面取得了很大的成就。1924年，菲尔兹筹办在加拿大多伦多市举行的第七届国际数学家会议时，节余了一笔费用。他建议以此作为基金设立国际数学奖，奖励那些在数学中作出重大贡献的数学家。1932年8月9日菲尔兹在多伦多去世了，遗嘱中表示把 自己留下的一大笔钱和第七届国际数学家会议节余的费用合并在一起转交给 1932年在苏黎世召开的第九届国际数学家会议，作为设置奖金的基金。并表示 不要用个人、机构的名称作为奖金的命名，而用“数学国际奖”来称呼。但鉴于菲 尔兹在数学界的威望和出于对他的缅怀，第九届国际数学家会议一致通过以“菲 尔兹奖”为国际数学家的最高奖赏。

11、菲尔兹奖的获奖人，由国际数学联盟执行委员会指定一个8人评定委员会来遴选。首先，从各方面提出40人左右的候选人名单，在广泛听取意见的基础 上，最后由评定委员会从中投票选定。在四年一度的国际数学家大会的开幕式 上，由执委会主席宣布得奖名单，然后授予获奖者一枚金质奖章及1500美元奖 金，最后由一些权威数学家来介绍得奖者的工作。第一次评奖在1936年挪威奥斯陆举行的第十届国际数学家会议上开始。当时世界上并没有对菲尔兹奖有多大的重视，后来菲尔兹奖的地位与日俱增，今 天菲尔兹奖被公认为数学界的诺贝尔奖。设立菲尔兹奖有一条不成文的规定：获奖者不能超过40岁。需要说明的是， 维尔斯因为证明费马大定理，于1998年破格获得菲尔兹奖，获奖当年45岁。有一位华人数学家丘成桐获得菲尔兹奖。丘成