数学腾讯文章

2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA1/11纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化↑点击订阅,了解世界科技最新动态版权属于世界科技欢迎个人转发到朋友圈、公众号、报刊等转载授权请联系wechat@wspc.
com吴文俊与中国数学机械化前言中国著名数学家吴文俊先生于2017年5月7日7时在京不幸逝世.
世界科技出版社于2008年出版了《SelectedWorksofWen-TsunWu》,收录了吴先生各个时期在不同领域的重要作品.
2017-05-09高小山WorldScientific2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA2/11Author:Wen-TsunWu2010年世界科技又出版了由姜伯驹,李邦河,高小山,李文林主编的《吴文俊与中国数学》一书.
此书是庆贺吴文俊先生九十华诞的中文文集.
集内的50多篇文章邀请了数学界的名家、友好和学生们,从不同的视角撰文介绍吴先生在拓扑学、数学机械化和古今数学史研究等三个方面的学术成就,对推动中国数学事业发展作出的杰出贡献和他的高尚品德,表达了数学界同仁对吴先生的共同景仰之情.
2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA3/11Editedby:姜伯驹,李邦河,高小山,李文林杨振宁教授杨振宁教授在序中说:"吴文俊的独立思考、开辟新领域的研究风格会给很多中国年青数学家鼓励与启发.
"姜伯驹教授姜伯驹教授在序中说:"吴先生得到数学界的特别爱戴,不只因为他多方面的学术成就,不只因为他平和公正的品格.
他有着深厚的爱国情怀,眼光远大,与我们一起亲历过风浪和曲折,亲身感受数学界的呼声,所以他的看法更切实,更有说服力.
他以自己顽强的探索与实践,鼓舞了我们的自信心,告诉我们要勇于思考,勇于走自己的路.
"吴文俊吴文俊1919年5月12日出生于上海.
1940年毕业于上海交通大学,1946年到中研院数学所工作.
1947年赴法国斯特拉斯堡大学留学,1949年获得法国国家博士学位,随后在法国国家科学中心任研究员.
新中国成立后,吴文俊于1951年回国,先后在北京大学,中国科学院数学研究所,中国科学院系统科学研究所、中国科学院数学与系2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA4/11统科学研究院任职.
曾任中国数学会理事长、中国科学院数理学部主任、全国政协常委、2002年国际数学家大会主席,中国科学院系统所名誉所长.
1957年当选为中国科学院学部委员(院士).
吴文俊对数学的主要领域—拓扑学做出了重大贡献.
他引进的示性类和示嵌类被称为"吴示性类"和"吴示嵌类",他导出的示性类之间的关系式被称为"吴公式".
他的工作是1950年代前后拓扑学的重大突破之一,成为影响深远的经典性成果.
1970年代后期,他开创了崭新的数学机械化领域,提出了用计算机证明几何定理的"吴方法",被认为是自动推理领域的先驱性工作.
他是我国最具国际影响的数学家之一,他的工作对数学与计算机科学研究影响深远.
吴文俊曾获得首届国家最高科技奖(2000)、首届国家自然科学一等奖(1956)、首届求是杰出科学家奖(1994)、邵逸夫数学奖(2006)、国际自动推理最高奖Herbrand自动推理杰出成就奖(1997).
数学机械化纲领吴文俊于1978年发表几何定理机器证明的第一篇论文后,主要精力转向数学机械化研究.
他不仅提出了数学机械化的主要方法,还花了大量时间遍寻各种可以用他的方法解决的应用问题,并亲自动手编制计算机程序给出这些应用问题的具体解答.
对此,有些同行表示不理解,认为吴应该继续致力于像拓扑学那样的核心数学领域.
但是,吴文俊从不为所动,2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA5/11""究其原因,是因为吴文俊关于数学机械化的研究体现了他自上世纪七十年代末形成的关于数学发展的观点.
1974年,吴开始研读中国数学史文献.
他发现,中国古代数学的显著特点是其构造性与算法化,而且算法化思想在数学的发展中起到了非常重要的作用.
吴文俊指出:回顾数学发展史,主要有两种思想:一是公理化思想,另一是机械化思想.
前者源于希腊,后者则贯穿整个中国古代数学.
这两种思想对数学发展都曾起过巨大作用.
从汉初完成的《九章算术》中对开平方、开立方的机械化过程的描述到宋元时代发展起来的求解高次代数方程组的机械化方法,对数学的发展起了巨大的作用.
公理化思想在现代数学,尤其是纯粹数学中占据着统治地位.
然而,通过数学史可以发现数学多次重大跃进无不与机械化思想有关.
例如,对近代数学起着决定作用的微积分也得益于经阿拉伯人传入欧洲的中国数学的机械化思想.
因此,吴认为应该重视机械化思想对于数学发展的作用.
机械化思想在数学研究中在过去未能得到足够重视,主要有两个的原因.

在理论上,机械化方法是不完备的.
逻辑学家对于定理证明机械化的探索,得到的结论大都是否定的.
例如,Godel证明初等数论的机械化是不可能的.
即使是正面的结果,例如,Tarski关于初等代数可机械化证明的算法也太过繁琐,以至于不能证明非平凡的定理.

鉴于此,吴文俊提出虽然不是所有的数学分支都可以机械化,但是确实有很多非常重要的数学分支是可以有效机械化的.
从方法上,适用范围太大的方法,如理论上可以证明所有定理的归结法,其效率必然低.
应该针对具体的数学分支发展特殊的高效算法.

在实践方面,机械化思想的实际应用需要大量的计算.
而人的计算能力是有限的.
计算机的出现使得数学的机械化成为可能,从而会对数学的发展起到重大的影响.
吴讲到"不久的将来,计算机之于数学家,势将与显微镜之于生物学家,望远镜之于天文学家那样不可或缺.
计算机提供了一个有力工具,使数学有可能像其他自然科学一样,跻身科学试验行列.

吴文俊进一步提出,数学的机械化不仅对于数学有重大意义,而且还在新的技术革命中扮演重要角色.
这是因为,数学的机械化将带动脑力劳动的机械化.
"枪炮的出现使人们在体力上难分强弱,而个人用计算机将使得人们在智力上难分聪明愚鲁.
"但是,也不必妄自菲薄.
大量繁复的事情交给计算机去做了,人脑将仍然从事更富有创新性的劳动.
2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA6/11"""数学是典型的脑力劳动,因此在脑力劳动机械化过程中有其特殊地位.
不仅如此,数学是自然科学与高科技的理论基础,数学方法的创新有可能带动科学发展与技术进步.
因而,数学机械化又有其迫切性.
此外,数学具有表达精确、论证严谨等特点,数学机械化在各类脑力劳动的机械化中又易于实现.
基于以上思考,吴文俊在写于1979–1981年期间的几篇文章中明确提出了发展数学机械化的重要性,并给出了后来称之为"数学机械化纲领"的指导思想:"在数学的各个学科选择适当的范围,即不至于太小以致失去意义,又不至太大以致于不可机械化,提出切实可行的方法,实现机械化,推动数学发展.
吴还特别重视数学机械化的应用.
他在973项目答辩时说道"应用是数学机械化的生命线.
吴自己关于数学机械化的研究也遵循以上想法.
吴选择了初等几何定理的机器证明作为突破口.
这是因为:几何推理自古以来被认为是推理的典范,以困难和技巧强著称,而且自1950年以来多位计算机学家进行了探索,但没有找到好的方法.
吴借鉴了著名逻辑学家王皓提出的以计算量的复杂来换取质的困难的思想,将初等几何定理机器证明问题转化为代数几何中方程解集的包含问题,从而提出了几何定理机器证明的第一个高效算法,取得了几何定理机器证明的突破.
以下引用1997年吴文俊获得国际自动推理最高奖"Herbrand自动推理杰出贡献奖"授奖词(AutomatedDeduction,1997,Springer),其中对吴的工作给予的详尽描述与评价.
吴文俊在自动推理界以他于1977年发明的(定理证明)方法著称.
这一方法是几何定理自动证明领域的一个突破.
""几何定理自动证明首先由HerbertGerlenter于五十年代开始研究.
虽然得到了一些有意义的结果,但在"吴方法"出现之前的二十年里这一领域进展甚微.
在不多的自动推理领域中,这种被动局面是由一个人完全扭转的.
吴文俊很明显是这样一个人.
""吴的工作由八十年代初期在德克萨斯大学学习的周咸青介绍给了西方学术界.
周咸青(基于吴方法)的证明器证明了数百条几何定理,进一步显示了吴方法的潜力.
至此,几何定理证明的研究已全面复兴,变为自动推理界最活跃与成功的领域之一.
""吴继续深化、推广他的方法,并将这一方法用于一系列几何.
包括平面几何,代数微分几何,非欧几何,仿射几何,与非线性几何.
不仅限于几何,吴还将他的方法用于由Kepler定律推出Newton定律;用于解决化学平衡问题;与求解机器人方面的问题.
吴的工作将几何定理证明从自动推理的一个不太成功的领域变为最成功的领域之一.
在很少的领域中,我们可以讲机器证明优于人的证明.
几何定理证明就是这样的一个领域.
2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA7/11"数学机械化理论与方法吴文俊关于几何定理机器证明的方法主要依赖一种关于代数几何的构造性理论.
吴早在上世纪六十年代就在中国科大开设了代数几何课程,"代数簇"一词即由吴文俊翻译命名.

吴于1965年前后引进了具有奇异点的代数簇的陈省身示性类,早于国外类似工作十余年.

在上世纪七十年代末,为了几何定理机器证明的需要,吴发展了美国数学家Ritt关于特征列的理论,提出了以吴–Ritt零点分解定理为核心的构造性代数几何理论.
代数几何是近代数学的核心分支.
长期以来,形成了各种流派.
当前流行的代数几何研究方法大都是存在性的.
近二十年来,代数几何的构造性理论也蓬勃发展,并在诸多的方面得到重要应用.
除吴–Ritt零点分解定理外,还有Groebner方法、周炜良形式等构造性方法.
评价与影响吴文俊关于数学机械化的工作获得国内外学术界高度评价与重视.
具体表现在以下几个方面.
1高度评价早在1982年,美国人工智能协会主席W.
Bledsoe和两位McCarthy奖获得者R.
S.
Boyer、J.
S.
Moore联名致信我国主管科技工作的领导人,赞扬吴的工作是最近十年中自动推理领域出现的最为激动人心的进展.
他们认为:"在过去两年中,我们这个领域(自动推理)最好的工作之一是吴的工作.
吴的平面几何自动定理证明的工作是一流的.
他独自使中国在该领域进入国际领先地位.

论文(W.
T.
Wu,Basicprinciplesofmechanicaltheorem-provinginelementarygeometries)是吴文俊关于数学机械化工作最重要的论文,给出了方程求解的特征列方法与几何定理机器证明原理.
本文后由国际自动推理权威杂志JAR全文转载.
JAR编委专门为转载写了短评(JAR,2,219–220,1986),对这一论文给予高度评价.
其中提到:"几何是激发人类思考'我们怎样推理'这一问题的最古老的数学分支之一.
因此几何自动推理的任何进展都特别有意义.
由中国科学院系统科学所杰出中国数学家吴文俊完成的如下论文,不仅建立了几何高效推理的基础,而且马上建立的一个杰出的标准来衡量以后出现的几何定理证明器.
2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA8/11"""""JAR主编Kapur在他的多篇文章中引用吴的工作,称"吴的工作使几何定理自动证明领域得到复兴.

他认为"可以毫不夸张地说,吴的工作使几何自动推理领域发生了革命性变化.
吴的初始工作以及吴和其它人的后续工作是过去十年中自动推理领域中最重要的进展.

Kapur本人还研究吴方法的各种改进,并将吴方法用于定理证明与计算机视觉.

自动推理领域创始人之一,JAR前主编L.
Wos认为"吴在自动推理领域的杰出贡献是不可磨灭的,没有一个数学领域象自动推理这样从一个人那里得到这样多的贡献.
吴文俊与DavidMumford于2006年共同获得邵逸夫数学奖.
吴文俊获奖主要是由于他对于"数学机械化这一交叉领域的贡献".
授奖词中提到:"吴的这一方法使该领域发生了一次彻底的革命性变化,并导致了该领域研究方法的变革.
通过引入深邃的数学想法,吴开辟了一种全新的方法,该方法被证明在解决一大类问题上都是极为有效的,而不仅仅是局限在初等几何领域.
2广泛影响吴的工作自八十年代中期传到国外,引起了国际自动推理与计算机代数领域的高度重视.
一些情况可以参见本书中周咸青教授的回忆文章.
吴的工作使得几何定理自动证明与以之有关的消去法研究变为热门的研究方向.
国外大学与科研机构连续召开研讨会介绍这方面内容.
其中有:(1)"GeometricReasoning",OxfordUniversity,1986.
会议文集作为国际著名刊物AI的专集出版,后又在MIT出版社出版.
(2)"Computer-AidedGeometricReasoning",INRIA,France,1987.
(3)"InternationalWorkshoponAlgorithmicAspectofGeometryandAlgebra",Cornell2017/5/9纪念吴文俊先生系列文章(一)---吴文俊与中国数学机械化https://mp.
weixin.
qq.
com/s/whFcmBkgM3CDz_Ax9QsLiA9/11University,1988.
很多有影响的国际会议如ACM–ISSAC(符号计算)与CADE(自动推理)还设关于吴方法的分会.
目前,关于数学机械化的国际会议有"几何自动推理"系列会议与"亚洲计算机数学"系列等会议.
吴方法被编入国际上非常流行的符号计算软件MAPLE.
关于几何定理证明的吴方法被编入"几何专家"软件,并在科技界与台湾与国内数百所中、小学中使用.

Springer、Kluwer、MIT、Academic、WorldScientific等出版社出版了关于吴方法的专著.
其主要内容是关于吴方法的改进与应用.
吴方法还在由Springer出版的研究生与大学生教材与专著中被列专门章节介绍.
3众多奖励吴文俊相继荣获第三世界科学院"数学奖"、陈嘉庚基金会"数理科学奖"、香港求是科技基金会"杰出科学家奖".
特别是,1997年获国际自动推理最高奖"Herbrand自动推理杰出成就奖".
该奖的获奖人包括自动推理创始人之一LarryWos,自动推理创始人之一、前美国人工智能学会主席WoodyBledsoe,归结法的发明人AlanRobinson等.
2000年获得首届国家最高科技奖.
2006年获得有东方诺贝尔奖之称的邵逸夫数学奖.