·刘卓军·
【真快，一年了，去年的5月7日晨吴文俊教授离开了我们。他的音容相貌还留在脑海中。我是吴先生的学生和同事中最后一位陪伴他的人。因为意识到他的时间不多了，5月6日下午我打电话给老吴的第一位博士毕业生王东明教授，让他赶到北京医院看吴先生最后一眼。尽管有心理准备，当第二天一早，吴先生离世的电话打来时，我还是非常悲痛和惋惜。
不久前，中国人工智能学会邀请我为吴文俊人工智能奖设立8年的活动写点文字，我答应了。第一稿刚刚完成，正好将这些文字在微信平台上发出来，以表达对吴先生的怀念。】
数学家吴文俊：1919.5.12 -- 2017.5.7
中国人工智能学会在2010年设立“吴文俊人工智能科学技术奖”，这是一件有历史意义的战略举措。8年来，通过该奖项的颁发，让我们鉴赏着、见证着中国人工智能领域取得的成果和人工智能事业发展的蓬勃态势。可以相信，伴随着学术界、产业界和社会对人工智能发展的高度关注与期待，吴文俊人工智能奖也必然会被更广泛地知晓，并激励着中国的专业人士、技术人士，尤其是有志的青年人才积极投身到人工智能的学术研究、技术开发和产业发展的潮流中。
吴文俊是著名数学家，其学术成果和贡献有着广泛的国际影响。然而，以一个数学家的名字来命名人工智能的重要奖项，总会令一些人充满好奇。但，这个安排又是那么的自然。2010年5月4日，国际小行星中心发布公报，将所发现并获国际永久编号的第7683号小行星命名为“吴文俊星”。尽管2017年5月7日吴文俊教授过世了，但他的学术影响永远留在地球上，他的精神将永远激励着我们。遨游在太空中的吴文俊星，一定会不停地遥望着我们的地球家园，或许会知晓我在此处写下的文字。我为曾是吴文俊的学生而自豪，也为他会认同我这里的一些看法和说法而自信。
数学家以讲严谨、重逻辑为主要特长。英国数学家伊恩·斯图尔特(Ian Stewart)在《现代数学的观念》(Concepts of Modern Mathematics)一书中曾经讲述了一个故事：
一个天文学家、一个物理学家和一个数学家乘坐火车在苏格兰旅行。从列车的窗口向外瞭望时，观察到天地中央有一只黑色的羊。“太神奇了，”天文学家说到，“怎么苏格兰羊都是黑色的！”物理学家纠正说，“不，不！应当说，某些苏格兰羊是黑色的！”数学家皱着眉头，严肃地说，“在苏格兰至少存在着一块天地，至少有一只羊，这只羊至少有一侧是黑色的。”
数学是理论、是方法、是工具。数学家常常有别于一般人的一些言语和举止，向社会和公众展现出非常真诚和可爱的一面。任何一门学科、一个领域，要想发展，要想成熟，不但需要干劲、冲劲，需要积累，还需要有可靠的基础，需要严谨和严密。大胆假设、小心求证，尤其是其中的求证非常需要数学方法和数学思想。从1956年算起，人工智能的发展已经经历了比一个甲子还长的时间。这一研究领域的总体状态一阵冷一阵热地交替变化着，从方法到内容一直都在发展和不断走向成熟。无论是从哪个角度审视人工智能的研究内容，实现自动推理、做到让计算机“自己”去证明定理既实现定理机器证明，这些都当然会是一项重要的研究课题。而在这方面，数学家吴文俊作出了杰出贡献，他建立起的一套方法及其所取得的成果得到了国际学术界的高度赞扬。仅从这一点看，以吴文俊这个数学家的名字命名中国的人工智能奖项，毫无疑问是非常恰当的。
一。人工智能：永远的挑战
很自然，人类首先要关心人本身的体能和智能问题。体能的问题似乎容易认识和理解，然而对智能概念的理解却仍然有很多需要深入思考的地方。和智能关联密切的概念当然应包含智商，通常描述成心理年龄和生理年龄的比，主要反映的是人的认知能力、思维能力、推理能力、计算能力、语言能力、观察能力、分析能力、反应能力、行动能力等。本质上，它主要表现的是有关人的理性的能力。这往往又要和感受、理解、运用、表达、控制和调节情感的能力有很大的关联，从而不可避免地要关联到情商的问题。可以说，认识智能问题既是基本的、重要的，又是充满挑战的。
1950年，图灵发表了一篇划时代的论文《计算机与智能》，预言人类创造出具有真正智能的机器是完全有可能的。由于注意到“智能”这一概念难以确切定义，所以他提出了著名的图灵测试：如果一台机器能够与人类展开对话而不能被辨别出其机器身份，那么称这台机器具有智能。图灵测试的一个伟大之处是，尽管我们对人自身智能的认识和理解永远都会在路上，但这并不妨碍我们追求和实现机器智能。
实现机器智能的目的之一就是利用计算机模拟、延伸和扩展人的智能。为此，需要对相关的理论、方法、技术及应用有系统深刻的认识和理解，这正是人工智能（AI）得以发展的根本原因，而1956年的达特茅斯会议当之无愧地被认为是人工智能时代开启的时间标记。人工智能具有典型的综合性和交叉性，不但具有理论，还具有技术和工程的特征。每出现一项大的社会进步和技术创新，都非常有可能扩大人工智能的范围，所以人工智能领域覆盖的内容将会与时俱进地发展变化着，而且将是不断扩大的。
对人类来说，没有体能就没法生存，没有智能就不能发展，就不能掌控世界。社会的不断进步已然出现了这样的局面：机器的发展代替了很多体力劳动，使人的体能得到了非常大的加强；计算机的发展则代替了很多脑力劳动，使人的智能也得到了显著的提升。一定意义上讲，人类的体能将是人辅以可控的机器所获得的综合体能，人类的智能将是人辅以可控的计算机所获得的综合智能。吴文俊1980年在为《百科知识》撰文时曾有过这样的论述：“不论是机器代替体力劳动，或是计算机代替某种脑力劳动，其所以成为可能，关键在于所需代替的劳动已经“机械化”，也就是说已经实现了刻板化或规格化。”按照这个观点，人工智能及机器智能永远都有进步的机会和发展的空间，这是因为人对世界的认识总会不断深入，总会不断地由表及里、由粗到细到精。只要我们对事物的认识进步到程式化、机械化的状态，我们就能够让计算机自动化地实现或模拟出相关的过程，而相伴的结果必然不同层面地体现着智能的发展。
图灵的伟大，不仅仅因为他提出了图灵测试，他是现代计算机科学和技术的奠基人。为了纪念图灵，成立于1947年，总部设在美国纽约的（美国）计算机协会（Associationfor Computing Machinery, ACM）1966年决定设立图灵奖（A.M. Turing Award），每年颁发一次专门奖励那些对计算机事业做出过重要贡献的个人。到目前为止，图灵奖的颁发已经进行了52届，共有67位科学家获此殊荣。其中，属于人工智能领域的有6个年份共8位科学家获得了图灵奖的认可。他们依次是，
1969年度的马文·明斯基（Marvin Minsky）
1971年度的约翰·麦卡锡（John McCarthy）
1975年度的艾伦·纽威尔（Allen Newell）和赫伯特·西蒙（Herbert AlexanderSimon）
1994年度的爱德沃德·费根鲍姆（Edward AFeigenbaum）和达巴拉·瑞迪（DabbalaRajagopal Reddy）
2010年度的莱斯利·瓦里安特（Leslie GabrielValiant）
2011年度的朱迪·颇尔（Judea Pearl）
获奖者中的明斯基、麦卡锡、纽威尔和西蒙都是1956年达特茅斯会议的参与者，他们因在人工智能领域中做出的有关研究框架理论的建立、函数式程序设计语言LISP的设计、通用问题求解器的开发、物理符号系统的提出以及把认知心理学和神经网络方法引入人工智能研究的有价值和有影响的工作，而成为人工智能领域的先驱式人物。费根鲍姆和瑞迪则因在展现人工智能技术的潜在商业价值和现实重要性做出的设计和开发人工智能系统的开拓性工作而获得奖励。瓦里安特的获奖基本上是归因于他发展的归纳学习方法对机器学习产生的重要影响，特别是该方法通过IBM沃森的表现而被社会所高度赞誉。颇尔的获奖则和他倡导人工智能的概率方法和贝叶斯网络技术而分不开，这种基于结果模型的因果和反事实推理方法对人工智能的进步作出了重大贡献。
近年来，随着AlphaGO的大出风头，人工智能技术受到了全社会前所未有的高度追捧。我们完全可以预期，支撑AlphaGO的各种关键技术，包括深度学习的有关方法，不远的将来也会受到图灵奖的表彰。然而，我们也需要理性地认识到，相对于人工智能的发展，一拨挑战过去，接着出现的将是另一拨挑战。热点如同风口一样，总会不断地变化。例如在当下，对于包括机器人和无人汽车驾驶技术在内的关注热情带给人们很大的憧憬，但要真正落地还有相当大量的工作要做。从战略角度看，大数据的发展，对人工智能的进步当然是非常重要的机会，但人才的问题、安全的问题、伦理的问题、技术的成熟问题，每一项都将充满着需要攻克的若干难点。越是希望在技术上取得重大突破和快速进展，就越应对人工智能的基础问题，基本问题有系统的深入理解。
下棋的程序和软件，不管它玩的是国际象棋还是中国象棋，甚或是围棋，机器赢了谁不是令人震撼的关键点，让人震撼的是，机器智能在一个令人感兴趣的点上与人比肩的能力取得的跨越式甚至是超过人的发展。
二。定理机器证明的突破性进展
随着计算机系统及计算机技术的成熟和发展，人们对让机器能模拟出体现着人类智能的兴趣越来越浓。做到这一点，具体地就是要通过机器来实现反映智能的各种能力。这其中，当然包括计算的能力、分析的能力和推理的能力。一旦机器成功地实现了对一种能力的模拟，就可以让具有这一能力的机器或程序辅助人、甚至代替人去处理相关事务。这个意义上讲，机器智能的提高也就促进了人的智能的加强，至少会解放人的一部分需要展现智能的脑力劳动。例如，我们可能谁都不会拒绝使用计算器来进行一些日常的计算，这是人的计算能力得以增强或是一些琐碎的、“繁重”的计算得以解放的证明。
或许体现人类智能的最主要的能力就是推理能力！这种能力是否能够通过机器模拟的方式得到加强？答案当然是肯定的，只不过在这方面即便是取得了令人鼓舞的结果，这个过程也将是漫长的，或许要伴随人类生存发展的始终。如何检验推理和分析能力是否得到了提高？一个非常有效的方式，就是让机器去自动进行定理的证明、判定！就如同做类似的图灵测试一样。
让机器代替人“干活”，这是人的聪明和智慧，也是人类智能的体现。人类的发展史上一直都在使用工具（和机器）助力体力增强体能。进一步，用机器助力脑力增强智能，很早也成为了人类的追求。例如，算盘的发明和使用就是一个非常好的说明。到了十七世纪，世界上第一台能计算的工具发明制造，其初衷正是为了助力人的计算能力。目的很明确，帕斯卡发明加法器就是希望能用机器更快更不易出错地进行税务方面的计算。帕斯卡的创造对几乎与他同时代的莱布尼茨的影响是巨大的，而且毫无疑问也影响到了今天计算机技术的发展。
莱布尼兹比帕斯卡思考的更深刻，他信仰大量的人类推理可以归约为某类运算。为此，他提出了建立万能符号语言和演算推理器的宏伟计划。他认为，精炼人类推理的唯一方式是使它同数学一样切实，这样我们就能一眼找出推理中的错误，在人们有争议的时候可以简单而平静地说：让我们坐下来计算一下，看看谁是正确的。
莱布尼兹是创造运算符号的大师，今天人类仍在使用的微积分符号就是他的贡献。在自动推理方面，300多年前他就坚定地认为，人类的观念和概念都是由数目有限的简单观念和概念复合而成的，即首先有一个人类思维的基本字母表；而复杂的观念则是通过类似于算术运算的操作对简单观念组合而成。可以这样讲，人类对自动推理的系统化认识和形成可行的问题解决方案，正是开始于莱布尼兹的伟大创举。历史跨越发展到上个世纪中期，现代电子计算机出现之后，利用机器，确切地说是利用计算机实现自动推理的莱布尼兹之梦才逐步成为现实可能。如何验证或证明自动推理的实现？让计算机能自动地证明定理，这是一个最为过硬的衡量指标。那么，应选取什么问题作为标的？考虑逻辑问题，考虑几何问题，这应是最基本、最基础的起步问题，这两类问题在人类智力发展、智能提升的过程中一直是最吸引人的。
1956年，也就是召开达特茅斯会议的那一年，纽威尔和西蒙等人开发出了一个称为“逻辑机器”的程序，证明了罗素、怀德海所著《数学原理》中的38条定理。1959年，格伦特尔等人用FORTRAN语言编出了一个称为“几何机器”的程序，能够做一些简单的中学几何题，速度与学生相当。1960年，美籍华裔教授王浩开发出了主要是进行命题逻辑的证明器，能自动证明罗素、怀德海《数学原理》中的几乎所有定理。在自动推理的方法上，1965年鲁滨逊建立了归结方法，使得自动定理证明的理论支撑有了进一步的增强。开拓性的工作不少，但能够自动证明的定理的“难度”也是人们普遍关心的问题！在这一点上，最初的自动推理程序和系统之能力展现还离人们的希望相去甚远。十多年后的1976年，阿佩尔和哈肯宣布通过计算机程序证明了四色定理，这的确是一件非常轰动的事情。然而，冷静地看，这不是定理的自动证明，顶多是定理的辅助证明。自动推理追求的不是“一理一证”，不是辅助性的证明，而是“一类一证”和“万理一证”，是真正的自动证明。
应当说，直到1980年代，从所用方法的“威力”和证明问题的难度上看，定理机器证明才算真正取得了突破性进展。
1983年，全美定理机器证明学术会议在美国科罗拉多州举行。一位由中国大陆赴美求学的青年学者周咸青，在会议上作了题为《用吴方法证明几何定理》的报告。周咸青开发的通用程序能自动证明130多条几何定理，用时不到半小时。在所自动推导出的结果中就包含很不平凡的莫勒定理、西姆松定理、费尔巴哈九点圆定理和迪沙格定理等的证明。周咸青取得的突破性成果在国际自动推理领域反响重大。而周咸青所使用的方法正是吴文俊教授建立和发展的定理机器证明的整序方法。这次会议的文集作为美国《当代数学》系列丛书第29卷于1984年正式发表。该文集同时收录了吴文俊教授的两篇相关论文。文集主编、曾任美国人工智能协会主席的布莱索教授，在序言中高度赞扬了吴方法。之后的1986年，在国际《自动推理杂志》主编穆尔教授的请求下，该杂志重新发表了吴文俊1984年已经在中国国内期刊上发表过的关于几何定理自动证明的奠基性论文《初等几何定理机器证明的基本原理》，这在国际学术期刊交流平台上是很难见到的情形。
由于意识到几何问题推理的重要性，《人工智能》杂志副主编、牛津大学布雷迪教授，美国康奈尔大学教授、1986年图灵奖获得者霍普克罗夫特以及通用电气公司的芒迪教授共同策划和组织了1986年6月30日至7月3日在牛津大学基布尔学院举行的几何自动推理的研讨会。1988年12月，国际《人工智能》杂志第37卷一至三期合刊特辑，收录了这次有35人参加的研讨会的部分报告。特辑的主编卡普尔和芒迪在特辑的引言文章中认为，吴文俊提出的代数几何的新方法相当成功，为几何推理的进步作出了巨大贡献。他们还进一步指出，几何推理除自身的重要意义之外，在人工智能的三大应用问题中：机器人和运动规划，机器视觉以及实体建模也都具有重要的应用价值。
上述这些前前后后的学术事件，无可争议地树立起了吴文俊的学术影响力，也非常有说服力地把吴文俊的名字与人工智能的概念自然而紧密地联系在了一起。
人工智能杂志发特刊，传播和讨论吴文俊创立的方法及其应用成果。
三。吴文俊及吴文俊方法
吴文俊是中国著名的数学家，享有很高的国际声望，是我国首届国家最高科学技术奖的获得者之一。他1919年出生于上海一个知识分子家庭。按他自己的表述，他更喜欢物理而不是数学。1940年在上海交大数学系毕业后，时值抗日战争，在中学教书约五年半。抗战胜利后，有机会在上海交大临时大学数学系任助教，得以从事数学研究。1946年有缘见到比他年长8岁的陈省身并受其影响和指导研究拓扑学。吴文俊天赋很高，上手很快，经陈省身的推荐于1947年底赴法国深造，1949年获法国国家博士学位，其间在拓扑学示性类研究方面做出了出色的工作。1951年学成归国的吴文俊先后在北京大学和中科院数学所供职，继续从事拓扑学的研究，因其在拓扑学示性类及示嵌类方面的学术成果而获得1956年国家颁发的第一届自然科学奖一等奖，第一届自然科学一等奖的获得者还有两位，他们分别是华罗庚和钱学森。之后的1957年，吴文俊被增选为中国科学院学部委员。这些学部委员共有190位，是新中国科技界的宝贝，他们也是后来中国科学院院士的最早成员。2017年5月7日，吴文俊作为这190位院士的最后一位离世了，某种意义上象征着一个时代的结束。
从问题出发
从问题出发，以问题带动学科的发展，这是吴文俊毕生坚持的观念。不论是发展理论还是创立方法，解决问题是根本，绝不应不知所以然地单纯追求从理论到理论，从方法到方法。一般说来，问题本身有基础性的问题，也有应用性的问题，或许是因为他的物理情结，他在晚年更加关注应用问题，包括在高科技领域提出的一些应用问题。而且身体力行，对一些应用问题的解决花费了相当大的心血。
吴文俊在数学研究的学术贡献，很多文字将其概括为出现在三个领域，即拓扑学、数学机械化和中国古代数学。从时间上看，我以为大致可以分为两个阶段，就是以七十年代前后划线。七十年代之前，吴文俊的研究精力主要花费在拓扑学上，他在这一阶段的研究成果属有重大影响的基础理论。相关的研究工作从发表文献的时间上看，一直持续到1975年前后。其实，他的研究兴趣是广泛的，例如在1960年前后，他还一度发表过博弈论及数学在国民经济中的应用等文章。这或许和中国社会发展的阶段特征有直接的关系，然而这种阶段特征在后来的恶化不但影响了他个人，也影响了整个中国的科技界。对于他个人来说，1966年至1973年期间，没有发表过任何文章，直到1974年之后，才又开始恢复发表研究论文。其中自然少不了关注体现应用特点的问题，如线性图的平面嵌入（1974年）和印刷电路与集成电路中的布线（1978年）问题。可以这样说，如果没有拓扑学方面的理论造诣和对实际问题的分析观察，是很难写出这类应用文章的。
还有一件多少属于具有标志性的事，1975年吴文俊在数学学报上第一次发表了关于中国古代数学的文章，“中国古代数学对世界文化的伟大贡献”。他用了笔名：顾今用。我们有理由确信，他想要表达的就是“古为今用”的寓意。从这个时点开始，他在后来正式发表了十多篇和中国古代数学有关的文章，他还于1986年在美国加州伯克利召开的世界数学家大会上作过题为“中国古代数学史最新研究”的45分钟学术报告。吴文俊后来多次说过，很多因素影响到他从事定理机器证明及数学机械化的研究，其中对中国古代数学的研究，给予他的帮助很大。他后来甚至专门撰文“复兴构造性的数学”，宣传鼓动要大力弘扬中国古代数学的思想。在他看来，推理式的做法和推算式的做法是非常不同的。
吴文俊第一篇关于定理机器证明的文章，“初等几何判定问题与机械化证明”发表于1977年，考虑的对象是关于几何问题的。在数学上，关于拓扑学有个比喻式的说法，称之为橡皮膜上的几何学。对于几何问题的分析和研究有拓扑学方面的造诣肯定是有帮助的。这样一关联，一联想，吴文俊在三个领域：拓扑学、数学机械化及中国古代数学作出有影响的工作，绝不是偶然的，某种意义上，它们是融会贯通的。
1971年，中国仍处在病态时期，研究人员需要参与“三个面向”：面向农村、学校和工厂。吴文俊提出到北京无线电一厂，下厂劳动。在那里，他接触到了电子计算机。从此，对电子计算机的应用产生了浓厚的兴趣。考虑布线问题、考虑用计算机证明数学问题，应当说和这段经历有着直接的关系。
机器证定理
人的思想是锁不住的，即便大环境不好，想问题是无人阻拦的，也阻拦不了。数学家自然要想着借助计算机进行数学研究，从1976年冬天开始，吴文俊已经作好了必要的准备，正式开始了几何定理的机器证明研究。
开展定理机器证明及数学机械化的研究，对具有广博学识的吴文俊来说肯定具有优势，但也同样面临着很大的挑战。因为，这类研究工作不能完全只作理论、“纸上谈兵”，还要动手、要算、要通过编写计算机程序让机器算。中国近现代的病态历史时期到了1976年9、10月之后才算结束，这时科研人员才能够广泛地开始研究工作。当时的吴文俊58岁，花精力研究定理机器证明，要考虑新的问题、要学新的知识、要攻克新的难关。他了解和分析了这个问题的研究现状，形成了自己的一套解题办法。他的方法本质上是用代数的方法，用代数几何的方法来处理几何问题。方法是否可行，需要验证。当时的计算机条件不行，只能靠手算做验证！吴文俊一出手就考虑非常有难度的问题 - 费尔巴哈九点圆定理。验算过程中涉及到的最大多项式有数百项，“计算过程”是全部符号化的，计算过程不能有错误，自然需要多次计算验证。1977年的春节期间，吴文俊通过手算成功验证了他所提方法的正确性和可行性。他非常兴奋和振奋而没有自满，再接再厉，他又手算证了其他几个有名的几何定理。成功了，至此，他知道自己的方法通过了检验。之后的事，就是他的工作得到了支持和肯定，中科院支持他买了计算机，而他自己又开始了新的学习，学习计算机语言，学习编程序，不断地上机实验，成了研究所里年岁最大的“程序员”。而且，方法本身还要完善、要系统化、相关的知识要传授、思想要交流。都说，成功是靠奋斗而得到的，这话一点都不假。
一个问题、一类问题的解决，关键因素很多。其中至少要包含两个要点，即靠对问题本身的认识和理解，还靠选择了适当的方法和工具。不妨现在让我们领略一下吴方法的概貌吧。首先，一个重要的历史人物必须提及！
笛卡尔，法国人，主要的是一名哲学家、思想家。他很明确地指出过，思想必须从简单到复杂；复杂问题必须分成若干简单的部分来处理。“我思故我在”是他的名言。他认为，人类应能使用数学方法 - 也就是理性 - 来进行哲学思考。这样一种方法论的思想和对数学理性的钟情或许是笛卡尔提出建立坐标系来刻画几何问题，进而创立解析几何的动力所在。甚至可以把笛卡儿的所思所想概括成一个解决一般问题的路线图：
所有的问题都可以转变成数学问题，所有的数学问题都可以转变成代数问题，所有的代数问题都可以转变成解方程组的问题，所有解方程组的问题都可以转变成解单变元的代数方程问题。
就初等几何定理的机器证明问题来说，吴方法首先要确定几何问题本身的描述方式。笛卡尔的思想当然是必须的。例如，对于平面几何问题，涉及到的几何对象无非是点、线、圆（弧）、三角形以及它们之间的“关系”，对于“关键点”的坐标以参数和变量的记号标记它们，并根据解析几何的方法，把几何图形中这些坐标点所应满足的关系式用代数方程组表述出来，几何问题的条件可以这样表示，需要证明的结论也可以这样表示。这就是几何定理机器证明吴方法的第一步：问题的坐标化与代数化。从数学的观点看，经过这一步，平面的几何问题已经对应到了高维空间中有限个一般点之间应满足的有限个代数方程组的数学问题。接下去的一步是，确定这些代数方程组所决定的解。确切地说，我们需要知道由几何问题之条件对应的方程组的解与几何问题之结论对应的方程（组）的解的关系。
求解线性方程组是学理科和工科的大学生都会的事。当然，求解规模很大既变量数目很多的线性方程组并不是件容易的事。而对于非线性的代数方程组，或一般的多项式方程组来说，即便规模不是很大，其求解都是非常具有挑战的。数学有个专门的分支 - 代数几何，研究的核心问题就是关于代数方程组的求解。根理想、理想成员判定问题、代数簇、零点集、希尔伯特零点定理等都是与之相关联的概念和方法。总之，要解代数方程组、要有效地决定代数方程组的解的结构，不是件容易的事。吴方法的关键环节正是体现在这里。这需要有整体的系统化的处理：引入的表示坐标点的参量和变量要规定适当的顺序；对每个得到的多项式，要根据统一规定的方法，赋予一个指标 - 秩；对与几何条件对应的多项式方程组集合进行约化处理，将约化过程中得到的非零的多项式添加到这个集合中，使得这个集合不断扩大；还要在理论上证明，这个过程会在有限步内终止，既这个时候，我们可以在这个集合中找到一组多项式，它们依据前面提到的变量的序和多项式的秩的规定可以排成一个先后顺序。此时，扩大了的集合中其它多项式对这个排好序的多项式组依次作约化得到的结果均为零。这时，我们称这组依次排好的多项式组为“特征列”；下一步，检验与几何问题之结论对应的多项式是否可以对这个特征列做约化而成为零。不为零，原几何定理不成立，等于零，则得到这样的结论或结果，在一组非蜕化条件下，原几何定理是成立的。就几何定理机器证明来说，我们并不必真的要解出多项式方程组的解，只要能分析出几何条件对应的方程组的解排除蜕化情形全部包含在几何结论对应的方程的解就足够了。为了做到这些，我们需要反复用到一个基本的运算，选定一个主变元的两个多变元多项式的代余除法。这样的操作，交给计算机去做是容易的。尤其对于初等几何定理证明来说，在坐标引入时，自然地就规定了变量之间的顺序，得到的多项式方程基本也不会高于2次。即便如此，如果用手工来算还是不得了的事，试想一下，一个含8个变元的，每个变元最高次不超过2，“最坏”的情形，将包含6500多项。而吴文俊在手算验证其方法是否可行时遇到数百项的多项式，还要对这样“复杂”的多项式进行代余除法，其中一个环节出了错误，验证的工作就前功尽弃。足以说明数学家的毅力和志气。
推导物理定律
吴文俊让计算机自动证明几何定理，这仅仅是个开始。吴方法还能够派上很多用场。例如，物理定律的发现。
1986年吴文俊访问美国阿格尼国家实验室时，知悉嘎波里尔教授正为如何借助计算机和数学工具从开普勒定律推导出牛顿定律而绞尽脑汁。回国后，吴文俊用自己的方法通过计算机实现了这一推导，并因此博得了许多科学家的称赞。国际自动推理领域著名的科学家，阿格尼实验室的沃斯认为，吴文俊的这一成果对自动推理领域是一次极为重要的拓广，表现出了非凡的洞察力和智慧。我想以十分钦佩的心情顺便提一句，沃斯是一位双目视力极为微弱的学者。然而，这位有着伟大毅力的科学家，在评价科研工作时，却有着敏锐而明亮的目光。
牛顿和开普勒都是名留史册的人物。开普勒发现过的两个定律是这样的：
定律1：太阳位于行星移动而成的椭圆轨道的焦点上。
定律2：行星与太阳成的向量，在行星绕椭圆轨道运行时，相同的时间内，扫过的面积一样。
而牛顿发现的万有引力定律被描述成：
定律3：行星运动的加速度与其到太阳的距离之平方成反比。
定律4：行星的加速度向量指向太阳。
牛顿通过观测和实验从开普勒定律导出万有引力定律是一个重要的历史事件。但是如何通过理论推导来重现牛顿的伟大发现，这一点在现行的教科书中几乎没有触及。相反，教科书中大量地介绍了如何从牛顿定律推导出开普勒定律。科学上等价关系、等价原理的相互推导，其一来一去，难易程度是不一样的。这也正是嘎波里尔遭遇的困惑之原因。为了让计算机实现万有引力定律的推导，需要借助微分代数的概念。粗略地说，就是先用微分代数的语言，把上面四个定律分别用微分代数方程刻画出来。然后把它们中的前两个摆放在一起，得到一个联立的方程组，经过和前面类似的微分情形的整序过程，做微分特征列意义下的拟微分代数簇分解，最后分别检验相应于定律3和定律4的微分代数方程，在如上的各拟微分代数簇上是否相容。相容性的判断，大体上是通过计算一个微分代数方程对一个微分特征列的余式来实现的。余式为零既表明相容。计算机计算的结果当然是以余式为零结束的。事实上，上面的推导过程，说到底是个验证的过程。其实，还可以做得更令人惊奇一些。
假设对牛顿定律一无所知，仅仅从开普勒定律的微分代数方程描述出发，经整序操作，计算机会不断地产生出新的微分代数表达式，当然这个过程总会在有限步内停止。经过简单分析，我们可以发现，表达牛顿定律的微分代数表达式也在其中。这个计算结果相当于宣布：在假设开普勒定律的前提下，吴方法用计算机自动发现了牛顿定律。对于体现智能和拓展知识来说，验证是一个层次，发现是相对更高的一个层次。
李子明、王东明、吴文俊、刘卓军、高小山，1987年摄于清华大学主楼
1987年春，王东明、吴文俊、李子明、刘卓军在吴先生家交流讨论
数学机械化
2015年6月初的一天，我和几个同事陪同吴先生和他的老伴去北京昌平考察。在看到中国农业机械化科学研究院写在院墙上的大字标语“农业的出路在于机械化”时，吴文俊即刻大声而诙谐地说“数学的出路也在于机械化”。吴文俊长期以来反复强调机械化的思想最主要的是希望表达与数学的公理化方式的区别。这种思想最早出现在中国的古代数学成果中，本质的特征就是构造性、算法化，非常适合当代计算机科学与技术，当然也包括计算机数学的发展趋势。“所谓机械化，无非是刻板化和规格化。机械化的动作，由于简单刻板，因而可以让机器来实现，又由于往往需要反复千百万次，超出了人力的可能，因而又不能不让机器来实现。”社会在发展，技术在进步，数学也要发展，推进数学机械化“使数学的发展面临一个前所未有的新时代”。
1990年的8月，中国科学院和当时的国家科委决定支持吴文俊搭建一个研究平台。由于吴文俊关于定理机器证明的工作已经获得了重要的国际影响，科学院和国家科委理所当然地希望将这个平台命名为机器证明研究中心。但吴文俊认为这正好是正名的时机，于是这个平台取名“数学机械化研究中心”并得到了批准。概括地说，机械化数学，就是用计算机来促进和发展数学；而数学机械化则是通过计算机发掘数学更多的应用。通常情况下，机械化数学和数学机械化被看作是相同的。
计算机与数学相伴早已不是新鲜事，例如，关注数值计算的计算方法的研究和实践，早就和计算机密不可分。但数学机械化所强调的重点是不同的，这里特别注重的是符号计算。当然，不排斥数值计算，事实上更鼓励开展符号与数值的混合计算研究，这样做将促进数学的应用，打开新的局面。在数学机械化研究的方法框架搭建上，吴文俊鼓励引入新的内容，比如添加微分代数的要素、实代数几何的要素和有限特征的要素等。在发挥数学机械化应用价值方面，吴文俊更是旗帜鲜明地说，应用是数学机械化发展的生命线。难能可贵的是，在这方面他自己一直身体力行带头去做。
1988年《人工智能》特刊曾有专文指出，几何推理在机器人、机器视觉与物体曲面拟合中的应用价值。对于这类问题，吴文俊自己都有过深入研究。以机器人为例，吴文俊考虑过工业机器人PUMA560其机械手臂的位置与机器各关节应转动的角度的关系问题。依据机器人的设计原理，指定机器手臂的空间位置，需要通过求解运动学方程的方式来确定各个转动关节应转动的角度。如果采用通过数值迭代方法，不能保证确定出所有的解。一个自然的方式是寻找关于所有转动角度的封闭解，而吴方法是适用的。这表明相应的方法对于机器人的设计问题是非常有帮助的。数学机械化的特征列方法后来还被用于涉及到机械机构学的斯蒂瓦特平台设计及精密数控机床的设计开发上。1986年牛津大学人工智能研讨会召集人卡普尔和芒迪在学习和掌握了吴文俊方法之后，对机器视觉分析和过程控制方面的问题也应用吴方法做了很好的尝试工作，并以此更有效果地传播了吴文俊的特征列方法。
并非所有人都能担当提出思想、创立方法的旗手。但对更多的人来说，品鉴和体会有开创性有影响力的方法中的精髓和要点是有意义和有价值的。吴文俊创立和发展的数学机械化的特征列方法，其要点似乎可以概括如下：
第一. 解决问题的表述问题。一切从问题出发，为了解决问题，必须能有效地恰当地表述需要解决的问题。对几何问题，坐标化、代数化是这一步的关键。经过分析和尝试，特征列的方法可以有更大的应用范围，例如机器人问题、机器视觉问题等，所需要的前提是相应的问题能够通过代数方程来表述。所以，概括起来，第一步，就是问题的代数化表述问题。换句话，特征列方法可以适用于一切能够规约成代数方程组求解或解的结构判定的问题。为此，必要时，这一步还要加入微分处理的要素；
第二. 有限性问题。以算法的方式求解问题，必须保证算法在理论上能够在有限步内停下来。这一点是常识，但要确定一种方式或是一些指标来观测和说清楚有限性的必然性并不是容易的。特征列方法中的变量顺序的指定、相关联于每个受到关注的排列起来的多项式组的秩的规定，为的就是这个目的；
第三. 具有基本操作和加工的手段。算法的本质是有输入，有输出。必然要有操作手段对输入及中间结果进行加工处理，形成新的中间结果直到形成最后的输出。特征列方法中充当约化处理的就是基本的代余除法。这样的操作满足有限性的要求，而这是关键所在。
第四. 有效性和策略问题。理论可行和实际有效是衡量算法的重要标准。可行是必须的，但又是不够的。需要在空间有效上或时间有效上有体现，有些问题的解决需要在两方面的有效性上都有体现。特征列方法曾经考虑过变量引进顺序的原则规定问题、考虑过由于不唯一而带来的基列及升列的选择原则问题，也考虑过混合计算策略的问题。这其中，一定还存在着问题类别不同，策略应有所不同的需要深入考虑的问题。
数学机械化要进一步发展，相应的新的算法也就必须依据所要关注的问题而提出和发展，上述提及到一些要点以及还一时没有意识到的更关键的问题都需要不断地思考。
如果说，需要表述一下遗憾的感觉的话，我们没有从底层搭建起助力数学机械化的系统平台。数学家们的擅长是在算法层面做出贡献，而系统的实现的确需要有更擅长的专业技术人员来参与。系统实现的问题，过去是今后也将是一个挑战。
闻道有先后，术业有专攻。经济学家可以通过观察到一只黑羊的特殊现象而感慨，从而发包社会的需求问题；物理学家可以通过实验和归纳推理的方式来总结和概括人们对事物的认识；计算机科学家及技术人员将不辞辛劳地通过软件、通过系统实现来集成人们的认识成果，并为人类认识、适应和改造世界提供工具；数学家将以严格地数羊的风格和方式为人类智能战舰的前行起着保驾护航的作用。
四。未来的梦想
几起几落，人工智能现在受到了广泛的社会关注，这是好事，也是社会和技术不断进步的标志。从研究者的角度看，人工智能是什么？是计算机科学、心理学、哲学、数学、物理学、工程学？这个表单会填的很长。可以说，也是，也不是！一个风险小的说法，人工智能是综合学科，是交叉学科！所有领域的科学家和研究及技术人员都能从中找到自己感兴趣的问题，都能在其中发挥出自己的作用。
参考图灵测试的方式来认识和评价智能与智力并非是一种无奈，即便社会和技术有了大的发展，这种评价方式也会是一种选项。无论是考虑产品还是系统，如果它能够像人一样，下得一手好棋、有令人惊叹的驾驶技术、能说会道会交流、还能流利地掌握多种语言等等，甚至在所能想到的方面比人做得还好，这些当然是智能的体现。而这或许就是人工智能的主要追求。技术发展和进步的结果，呈现给人类的历来都是双刃剑。这或许是自然界，包括人类社会发展演变的宿命特征。
最后，我还希望就吴文俊在几何定理机器证明的研究中明确提出的“蜕化条件”概念谈一些体会。但凡对复杂的问题，要想建立一套放之四海而皆准的方法，往往是做不到的。认识和确定一种方法的适用范围和边界，需要智慧和勇气，需要严谨和洞察。以一个关联到三角形的几何问题来说，当我们断言一个命题时，通常会隐含地要求这个几何图形中所涉及到的三角形应当是一个一般化的、正常的三角形。比如，我们会排除这个三角形蜕化成一条线段的情形，如所论的三角形有两条边重合，并且有两个点重叠。对于几何定理证明来说，原始的问题是几何问题，转换后表述成代数的问题，这样的转换会带来相关信息的增或减。漂亮的是，吴文俊的方法能够发现这种蜕化的情形，并用一些多项式的初式来表述。这个发现对推理和证明的严谨性本身就是一个重要的贡献。我想借此说明的是，在我们发展数学机械化的方法拓展能够解决问题的空间时，对于可能带来的变化问题必须仔细分析。如果能够明确确定出一些约束条件的话，有可能这不是新方法的局限，而是对原问题认识和理解的深化。我相信，这样一种体会绝不仅仅会在机械化数学的研究中能够感受得到。
2004年，吴文俊参观中关村科技园区
吴文俊对学生的鼓励
社会每当在体现与人的智能可以比肩的产品和系统取得进步时，都会引发人们对人工智能的欢呼和期许。在大数据、物联网和云计算的技术不断成熟的情况下，这样的场景将会更为频繁地呈现。差不多可以这样认为，历史发展到今天，人类获取智能所遵循的就是一条从数据(data)到信息(information)到常识(knowledge)到认识(insight)到智慧(wisdom)的演变路径。而人工智能的终极发展，这个路径也极具价值。
数据多了、联网的智能设备多了、计算能力增强了，机器智能和网络智能必然会呈现普遍的增长。机器学习、深度学习等肯定会得到比以往任何时候都受到关注的方法。但要综合地整体地考虑系统智能时，方法上必须兼收并蓄。数学的方法、系统的观点将扮演着更加重要的作用。
世界是物质的、能量的、信息的、系统的。在这个认识框架下，数据是用于表示客观事物的未经加工的原始素材，它是对事实、事物、系统的观察或观测到的结果，形式上具有多样性。从人们的生活实践和社会实践来看，数据和信息不可分离，数据是信息的载体和表达，信息是数据的内涵，是经过加工了的数据，是数据处理的结果。这种认识和理解与信息论奠基人香农指出的“信息是用来消除随机不确定性”的本质并不抵触。
事实上，对于感兴趣的事实、事物乃至系统，如果获取的信息多，对其在认识上的不确定性或模糊性就会少。不难理解，人们对系统的关注和兴趣，根本的目的是要认识它、适应它、溶入它、“控制”它，乃至最终利用它并与其和谐相处。这其中当然需要智慧。机器智能、人工智能的发展将呈现更多的机会！（2018-5-6，第一稿）