吴文俊与几何定理机械化证明

【内容摘要】吴文俊是我国当代享誉世界的杰出数学家，人教版《普通高中课程标准实验教科书数学（必修2）》第四章圆与方程中的阅读材料“坐标法与机器证明”一文中，简单地介绍吴文俊和他的几何定理机器证明的思想。本人在教学中发现，许多中学生并不知道这位数学家，更不用说几何定理的机械化证明。本文旨在向广大中学生宣传吴文俊的学术成就和治学精神，说明几何定理机械化证明的思想和方法，激发中学生科学探究的兴趣和爱国主义情感，实现数学教材中阅读材料的价值。

【关键词】吴文俊 几何定理 机械化证明

吴文俊教授，我国当代享誉世界的著名数学家。1919年5月12日生于上海，1940年毕业于上海交通大学，1949年获法国国家博士学位。中国科学院数学与系统科学研究院系统科学研究所研究员、名誉所长，中国数学会名誉理事长。中国数学机械化研究的创始人之一，现任中国科学院系统科学研究所名誉所长、研究员，中国科学院院士，第三世界科学院院士。曾任中国数学会理事长（1985-1987），中国科学院数理学部主任（1992-1994）。

曾获得首届国家自然科学一等奖（1956）、中国科学院自然科学一等奖（1979）、第三世界科学院数学奖（1990）、陈嘉庚数理科学奖（1993）、首届香港求是科技基金会杰出科学家奖（1994）、Herbrand自动推理杰出成就奖（1997）、首届国家最高科学技术奖（2000）、第三届邵逸夫数学奖（2006）。

2010年5月4日，国际小行星中心先后发布公报通知国际社会，将国际永久编号第7683号小行星永久命名为“吴文俊星”。

1976年粉碎“四人帮”之后，中国迎来了科学的春天。年近花甲的吴文俊在中国古算研究的基础上，分析了西方R.笛卡儿的思想，深入探讨D.希尔伯特《几何基础》一书中隐藏的构造性思想，开拓机械化数学的崭新领域。数学机械化方法的思想是：从几何公理体系出发，首先取适当的坐标，于是几何定理的假设与终结通常都成为多项式方程，称之为假设方程与终结方程，满足定理假设的几何图像就相当于假设方程组的一个解答或零点。要证明定理成立，就是要证明假设方程的零点也是终结方程的零点。

1976年冬吴文俊开始研究，1977年春取得初步结果。证明初等几何主要一类定理的证明可以机械化，问题分成三个步骤：

“第一步，从几何的公理系统出发，引进数系统及坐标系统，使任意几何定理的证明问题成为纯代数问题。

第二步，将几何定理假设部分的代数关系式进行整理，然后依确定步骤验证定理终结部分的代数关系式是否可以从假设部分已整理成序的代数关系式中推出。

第三步，依据第二步中的确定步骤编成程序，并在计算机上实施，以得出定理是否成立的最后结论。”

1977年吴文俊在一台档次很低的计算机（长城203型台式计算机）上首先按上述步骤实现像西姆森线那样不很简单的定理的证明，然后又完成了西姆森线、费尔巴哈定理、毛莱定理等一系列初等几何的证明。并把机器定理证明的范围推广到非欧几何、仿射几何、圆几何、线几何、球几何等等领域，先后与其同伴们陆续证明100多条定理。周咸青应用吴氏算法证明600多条定理。1978年初吴文俊又证明初等微分几何中的一些主要定理也可以机械化。

吴文俊的成就在于：

（1）提出一套完整的算法，使得代数方程组通过机械步骤消元变成一个代数方程。

（2）解代数方程组可扩大为带微分的代数方程组，从而大大扩张研究问题的范围。

（3）不仅能证明定理，而且能自动发现定理，这大大优越于现有的任何方法。

（4）与许多以前的原则可行的方法相比较，吴文俊的方法完全是现实可行的。

（5）算法稳定，能一举同时得出多解，这是其他算法根本无法比拟的。

吴文俊几何定理机械化证明的方法，被世界数学界誉为“吴方法”，给两千多年的公理化演绎体系带来了强烈冲击。吴文俊的数学机械化思想不是一时心血来潮，而是长期思考导致的战略转变。他认清计算机出现对人类工作和生活的巨大促进，更认识到计算机对于未来脑力劳动机械化的潜在影响。要知道，当时还没有微机，微软也刚刚建立，没人想到十年之后、二十年之后的变化。吴文俊想的更远，他不仅看到体力劳动的机械化，更高瞻远瞩地看到脑力劳动的机械化。而数学正是最纯粹的脑力劳动。脑力劳动的机械化当然从数学做起，数学的两大任务是证明定理及计算，数值计算不成问题。问题是如何把证明化为符号计算并且由计算机实现，这就是数学机械化中心思想。

到80年代，吴文俊不仅建立数学机械化证明的基础，而且扩张成广泛的数学机械化纲领，解决一系列理论及实际问题。这仅仅是吴文俊数学成就的一小部分。此外他在拓扑学、自动推理、代数几何、中国数学史、对策论等研究领域均有杰出的贡献，在国内外享有崇高盛誉。

吴文俊取得这些成就完全是靠他一生积极进取、锲而不舍的治学精神。他读庞特里亚金的俄文原文完全是靠字典一个字一个字查出来的，使用计算机完全靠自己长时间一点一点摸索出来，其刻苦精神由此可见一斑。他热爱数学、独立思考、富于创见，无论外界环境顺利还是困难，都能始终如一地努力从事研究工作。吴文俊一生淡泊自守，对于名利看得很轻，从来不宣扬自己，以至于他在国内的知名度与他的成就显得极不相称。他不仅从未沾染学术界的一些不良作风，恰恰相反，他平易近人，乐于助人，乐于宣传其他人的成绩，学术作风民主。永远是青少年学习的榜样，数学工作者的楷模，中国数学界的一面旗帜。

【参考文献】

[1] 胡作玄.《吴文俊》.

[2] 人教版《普通高中课程标准实验教科书数学（必修2）》.

（作者单位：安徽省天长中学）