吴文俊与数学机械化

吴文俊与数学机械化纪志刚上海交通大学学报，2001年第3期摘要：机器证明的思想可以回溯到17世纪的Descartes与Leibnize，20世纪初Hilbert更明确地提出了公理系统的机械化判定问题。但是，随后的种种努力都未能使机器证明取得本质的进展。近20年来，吴文俊继承并发展了中国古代的数学思想，在定理机器证明上开创了以多项式组零点集为基本点的消元方法；吴文俊的数学机械化方法已在物理规律的发现、机器人学、计算机视觉以及促进现代数学研究等重大高科技的前沿领域实现了成功的应用。数学机械化研究的兴起，是中国当代数学发展中一个引人瞩目的具有中国传统特色的新里程碑。关键词：机器证明；数学机械化；中国古代数学；中图分类号：文献标识码：文章编号：WuWen-tsunandMathematicsMechanizationJIZhi-gang(DepartmentfortheHistoryofScience&PhilosophyofScience,ShanghaiJiaoTongUniversity,Shanghai200030,China)Abstract:TheideaofprovingtheoremsmechanicallymaybedatedbacktoDescartesandLeibnizeinthe17thCenturyandhasbeenformulatedinprecisemathematicalformsinthe20thcenturythroughtheschoolofHilbert.Inspiteofvigorousefforts,however,researchesinthisdirectiongiverisequiteoftentonegativeresults.Forexample,themethodsofTarskibasedonageneralizationofSturmarestilltoocomplicatedtobefeasible,evenwiththeuseofcomputers.ItisWuWen-tsunwhoestablishedanewalgorithmforthemechanizationoftheorem-provinginelementarygeometry.Wu’smethodswerealloriginatedandquitedevelopedfromancientChinesemathematics.Infact,thealgebrizationofgeometricalproblemsandsystematicmethodoftheirsolutionbyalgebraictoolsweresomeofthemainachievementsofclassicalChinesemathematics.Now,themethodofmathematicalmechanizationhasbeenplayedanimportantroleinmathematics,andgottenitswideapplications.Keywords:mechanicalproving；mathematicsmechanization；classicalChinesemathematics；WuWen-tsun一、机器证明：古老的梦想相传Ptolemy王曾向Euclid请教学习几何的捷径，Euclid没有屈从帝王的尊严，直率地说：几何中无王者之路(Thereisnoroyalwayingeometry)。以希腊的几何学为代表的古代西方数学，其特点是在构造公理体系的基础上证明各式各样的几何命题。几何题的证法，各具巧思，争奇斗艳，无定法可循，只有依赖个人的经验、技巧和灵感。学习几何的孩子做梦都在想：要是几何题象解一元二次方程那样多好。这种愿望由来已久，17世纪法国的数学家Descartes曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。”Descartes把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方程求解是可以机械化的。但Descartes没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，实现了初等几何问题的代数化。比Descartes晚一些的德国数学家Leibnize曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。Leibnize认为，他的方案一旦实现，人们之间的一切争论都可以被心平气和的机器推理所代替。他的努力促进了Boole代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。更晚一些，德国数学家Hilbert明确提出了公理系统中的判定问题：有了一个公理系统，就可以在这个系统基础上提出各式各样的命题，那么，有没有一种机械的方法，即所谓算法，对每一个命题加以检验，判明它是否成立呢？正是在Hilbert的名著《几何基础》一书中就提供了一条可以对一类几何命题进行判定的定理?当然，在那个时代，不仅Hilbert本人，整个数学界都没有意识到这一点。数理逻辑的研究表明，Hilbert的要求太高了。著名的Godel不完全定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！数学大师们坚持不懈地求索，表明数学机械化的思想重要而深刻；而数学机械化在历史上发展缓慢，同时也意味着这一方向道路漫长而艰难。证明的机械化，如果没有可以进行数学演算的机器，只能是纸上谈兵。电子计算机的问世，促使数学机械化的研究活跃起来。波兰数学家Tarski在1950年推广了关于代数方程实根数目的Sturm法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。1959年，著名数理逻辑学家，美国洛克菲勒大学王浩教授设计了一个程序，用计算机证明了Russell、Whitehead的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了9分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。特别的是，他第一次明确提出“走向数学的机械化”（TowardMechanicalMathematics）。1976年，美国两位年轻的数学家在高速电子计算机上耗费1200小时的计算时间，证明了“四色定理”，使数学家们100年来未能解决的难题得到肯定的回答。在数学发展的漫长历史中，积累了无数的几何定理。这里面有许多巧夺天功、趣味隽永的杰作。由于传统的兴趣和应用的价值，初等几何问题的自动求解遂为数学机械化的研究焦点。自Tarski的引人注目的定理发表以来，已经26年过去了，初等几何定理的机器证明，仍然没有令人满意的进展。在经过许多探索和失败之后，人们在悲叹：光靠机器，再过100年也未必能证明出多少有意义的新定理来！吴文俊的工作，揭开了机器证明领域的新的一页。二、吴方法：王者之路当中国的历史艰难地走出十年浩劫的磨难的时候，1977年，吴文俊在《中国科学》上发表的论文《初等几何判定问题与机械化问题》，为数学机械化领域送去了一缕清新的春风。1984年，吴文俊的学术专著《几何定理机器证明的基本原理》由科学出版社出版，这部专著遵循机械化思想引进数系和公理，依照机械化观点系统地分析了各类几何体系，明确建立了各类几何的机械化定理，着重阐明几何定理机械化证明的基本原理。1985年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。这篇重要文献，是正式建立求解多项式方程组的吴文俊消元法的重要标志。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的学术路线。自此，“吴方法”宣告诞生，数学机械化研究揭开了她新的一幕。几何问题的代数化是几何问题机械化的第一步，为此需要引进数系，建立坐标系，把几何命题的图中的各种关系利用代数方程来描述。在适当选取坐标系后，如果几何定理的假设条件可表示为一组代数方程[H]：f1=0，f2=0，…，fr=0，而几何定理的结论由代数方程C:g=0所刻画，这里f1,f2,…,fr和g都是变元x1,x2,…,xn的多项式，那么几何定理的机械化证明就归结为如下问题：机械化问题构造并提供一种确定的、机械的算法，使得依此算法进行有限步之后即可判定：在若干附加条件之下，结论C是否可由假设[H]推出，即是否可由f1=0，f2=0，fr=0推出g=0。由此可见，实现数学定理机械化证明的关键，在于必须对表示定理假设的多项式组[H]的零点集给出构造性的描述,以便区分多项式组[H]的零点集,从而可以确定在多项式组[H]零点集的哪部分之中,能够保证多项式g=0.吴文俊消元法（吴方法）恰恰完成了这项任务。因此，吴方法是定理机器证明吴文俊原理的理论基础，定理机器证明的机械化原理的建立是吴方法的成功运用。吴文俊原理设数学定理的假设条件由多项式方程组[H]＝0表示，定理的结论由多项式方程g=0表示。并设CS＝{A1,A2,….,Ak}为多项式方程组[H]的特征列。如果多项式g对[H]的特征列CS的余式R=0,则在条件Ii≠0,i=1,2,…,k之下,可从[H]=0推出g=0。条件Ii≠0,i=1,2,…,k称为数学定理成立的非退化条件。这组非退化条件是在计算特征列过程中自动产生的。非退化条件这一概念的发现,是吴文俊在数学机械化证明领域的突出贡献。这一概念的引进,实现了数学定理机器证明的决定性突破。一般说来,用吴方法判定一个命题,要分三步进行:第一步是把所给命题化为代数形式，即判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题;第二步是整序，即把刻划命题条件的多项式组[H]经整序化为升列AS；第三步是求余，即将刻划命题结论的多项式g对于升列AS约化求取余式R。若R=0，即可断定命题在非退化条件Ii≠0,i=1,2,…,k之下成立，或者说命题一般成立，其中I1,I2,…,Ik是升列AS中各多项式的初式。若R不为0,则当AS为不可约升列时,可断定命题不真。多项式方程组求解曾被认为是极为困难的问题,这已为它的研究历史过程所证明。但是,吴文俊消元法的叙述简明自然，顺理成章，结论易懂，方法易学。可以用相当短的时间向初学者介绍吴方法，并在计算机上具体操作吴方法的计算过程。初学者往往惊奇的发现：吴方法竟是这样的简单自然，感叹为什么别人没有发现它！事实上，将公认的难题，应用初等方法简朴自然地加以解决，是数学科学返璞归真的最高境界。三、《九章算术》：惟有源头活水来50年代，拓扑学刚刚从艰难迟缓的发展中走向突飞猛进，吴文俊敏锐地抓住了拓扑学的核心问题，在示性类与示嵌类的研究上取得了国际数学界交相称誉的突出成就。1956年荣获国家自然科学一等奖，1957年当选为中国科学院学部委员（现称院士）。那时他才38岁。作为一位年轻的数学家，这已是莫大的荣誉了。而对吴文俊来说，这只是在西方人开创的方向上做出的工作，新中国的数学家应该开拓出属于自己的研究领域。但是，路在何方呢？那就是数学机械化！是什么力量使得吴文俊从一位卓有成就的拓扑学家，走上数学机械化的研究道路呢？吴文俊在《吴文俊文集》前言中有过动情的叙述：作者关于机械化思想的形成，决非一朝一夕，至少在70年代以前，机械化的概念在作者脑海里还毫无踪影。经过对中国古代数学的学习和触发，结合着几十年来在数学研究道路上探索实践的回顾与分析，终于形成了这种数学机械化的思想。这种思想一旦形成，就自然地化成一股顽强的动力。十几年来，作者一直在这一方向道路上摸索前进，艰苦奋斗，义无反顾。70年代初，吴文俊开始研读中国数学史。中国古代数学曾有过辉煌的历史，直到14世纪，在许多数学领域都保持西方望尘莫及的水平。但是，西方一些数学史家不了解也不承认中国古代数学的光辉成就，将其排斥于“数学主流”之外。吴文俊对此作了正本清源的研究。19