我于1984年考入中科院系统科学研究所(后面简称系统所)攻读吴文俊先生的研究生。非常幸运,吴先生第一个学期就在中科院研究生院玉泉路校区开设了“机器证明”课程。我后来才知道,用的讲稿是他刚刚完成的数学机械化经典著作《几何定理机器证明的基本原理》的第4章。1985年春季学期开始后,吴先生又在中关村系统所开设了数学机械化讨论班。讨论班开设之初主要由我们几位研究生轮流讲W.V.D. Hodge和D. Pedoe所著的《代数几何方法》。吴先生在下面听讲,给予指点,并亲自讲了代数对应等章节。这段经历对我今后的发展产生了多方面影响,本文后面将会提及。
吴先生上世纪60年代初开始研究代数几何,并很快取得成果。1965年,他首次对于具有任意奇点的代数簇定义了陈省身示性类。很可惜,因文革爆发,吴先生未能继续发展这一工作,又由于论文是以中文发表,未能被国外同行了解,错过了一个重要的发展机会。在这一问题上后来由R.D.MacPherson等人做出了重要成果。但另一方面,吴先生对代数几何的研究为后来创立数学机械化提供了有力工具。实际上,构造性代数几何理论是吴先生开创的数学机械化的基本工具,数学机械化的核心算法即通过构造三角列将一般的代数簇分解为不可约代数簇的并。
1985年秋天我从玉泉路校区回到中关村园区开始在吴先生的指导下做研究。吴先生指导研究生的特点是不直接给题目。他总是将自己的最新成果或国际上最新发表的论文交给我们,让我们自己去领悟并找题目。学生们完成的成果,吴先生会认真研读,对喜欢的结果会说“这个很好”。我做的第一个工作是特殊函数恒等式的机器证明。按照师门的传统,我在系统所的HP1000小型计算机(是科学院当年为吴先生研究机器证明购置的高档计算机)上自己编程验证。我的本科专业是信息系统工程,学的课程多与计算机相关,所以对编程有一定基础。在一次无意的交流中,吴先生知道我编的多项式乘法运算程序比他编的要快,非常高兴并马上修改了自己的程序。后来,系统所的许国志先生告诉我,吴先生因此事曾向许先生夸奖过我。许先生后来参加了我的博士论文答辩,答辩委员会成员还有洪加威教授。受吴先生工作的影响,洪加威教授提出了机器证明几何定理的例证法。洪加威教授当时给我提的问题是,你证明定理是由假设推出结论,但是假设本身是否成立并没有验证。我当时没能很好地回答,这实际上是吴先生数学机械化理论的简单推论。
吴先生常常默默无闻地帮助他人。1987年美国德克萨斯大学Austin分校的周咸青博士来系统所访问。他希望我88年秋天获得博士学位后到他那里从事博士后研究。能够出国到名校工作,对我来说是莫大的惊喜。周咸青后来告诉我,1986年吴先生访美时对他讲,高小山虽然不是数学专业毕业的,但是在讲Hodge-Pedoe的《代数几何方法》时讲得最仔细,并向周咸青推荐了我。在德克萨斯大学工作的近三年是我研究上最多产的一段时间,完成了近10篇论文,包括我的首次发表在JAR,JSC,ISSAC,CADE上的论文。期间还认识了Bledsoe,Boyer,Moore等自动推理与人工智能领域的著名前辈。周咸青在Boyer,Moore指导下的博士论文也是关于吴方法和几何定理机器证明。关于周咸青与吴先生的结缘以及吴方法在国际上传播的介绍请见他撰写的《吴文俊先生和几何定理证明》。由于我在美国也研究数学机械化,所以在那里访问的很多华人与我开玩笑说:“我们都是来美国学习的,你是带着中国的思想来美国的。”
吴先生的工作于1984年以后在国际自动推理与符号计算界产生了巨大影响,获得了自动推理界知名学者W. Bledsoe, L. Wos, R. Boyer, J. Moore, D. Kapur等人的高度评价,多国学者竞相学习与研究吴先生的工作,他在国内发表的两篇论文分别被JAR与美国数学会出版的《当代数学》论文集全文转发(当时国外很难看到国内发表的论文),吴先生的工作成为多个国际学术会议的主要议题,国际人工智能旗舰刊物AI出版了吴方法的专辑。意大利的Carra-Ferro与Gallo是最早跟随吴先生研究机器证明的学者。2006年,我受邀赴意大利西西里岛参加Catania大学举办的纪念Carra-Ferro的微分代数会议。会议组织者Gallo在会议开幕式上讲到:20年前我们在同一个会议室开会,“会议的明星是吴文俊教授”。我由此依稀想象到1986年前后,吴先生在欧美各地讲学的盛况。
我于1990年底回国,错过了当年“数学机械化研究中心”的成立大会。国际上对吴先生工作的热烈反响反过来推动了国内的数学机械化研究。1990年国家科委拨款100万元专门支持数学机械化研究,中科院成立了“数学机械化研究中心”,吴先生任主任,程民德先生任学术委员会主任,日常工作由北京市计算中心的吴文达先生主持。北京大学的程民德先生长期支持并积极参与吴文俊先生倡导的数学机械化研究。程民德先生与石青云院士合作将吴方法应用于整体视觉,并指导研究生李洪波开创了几何定理机器证明的新方向。
我回国后赶上了由陈省身先生主持的“南开数学中心”于1991年举办的“计算机数学年”。这次活动由吴先生与胡国定先生负责,石赫教授常驻南开大学具体组织。学术年邀请了多位从事符号计算的专家访问中国,包括G.E. Collins, C. Bajaj, M. Mignotte, V. Gerdt等,也邀请了李天岩等计算数学专家。这是数学机械化领域开展的第一次大规模的学术活动。1992年在北京组织了第一次“数学机械化研讨会”,吴先生任会议主席,我负责了会议的具体组织事宜。会议在刚刚建成的中科院外专公寓举办,参与会议的国外学者包括C. Bajaj, G. Gallo, V. Gerdt, C.M. Hoffmann, D. Kapur, B. Mishra, T. Mora, H. Suzuki,周咸青等。这是我第一次组织国际会议。数学机械化研讨会后来发展成为系列会议,举办了十多次。2009年为了庆祝吴先生90岁生日举办了包括数学史在内的扩大版 “数学机械化研讨会”,我再次担任会议主席。与吴先生同为符号计算先驱的Bruno Buchberger与Daniel Lazard以及著名学者Komatsu Hikosaburo做了大会邀请报告。
1992年,国家攀登项目“机器证明及其应用”由国家科委立项,吴先生任首席科学家。项目设立6个子课题:机器证明的理论与算法、代数系统求解的理论与算法、吴方法在理论物理学中的应用、吴方法在计算机科学中的某些应用、吴方法在数学科学中的某些应用、吴方法在机器人机构学运动正解及其应用。杨路教授与我是第一课题的负责人。张景中、杨路教授于1987年左右开始从事数学机械化研究,培养了很多优秀学生,成为了数学机械化研究领域的一支重要方面军。张景中先生因几何定理可读证明的工作于1997年当选为中科院院士。
在国际上与数学机械化相近的研究领域是符号计算或计算机代数。符号计算领域最权威的国际会议是由国际计算机协会(ACM)符号与代数专业委员会(SIGSAM)组织的ISSAC,始于1966年。吴先生于1987年第一次在ISSAC做邀请报告。ISSAC'92在美国加利福尼亚大学 Berkeley分校举办,吴文达与我参加了这次会议,并在会上代表数学机械化研究中心提出在北京举办ISSAC '94的设想。申办ISSAC '94的另外两个城市是英国Oxford和加拿大Montreal。我们的申请得到了P.S. Wang和E. Kaltofen等人的支持,但未能成功。2003年我代表数学机械化中心再次申办ISSAC并获得成功。ISSAC 2005在北京成功举办,我与George Labhan任会议主席,吴先生第二次在ISSAC大会上做邀请报告。ISSAC是数学机械化团队在国际上展示成果的重要舞台,李子明、李洪波、高小山等先后获得ISSAC最佳论文奖,我们的团队被M.Singer称为“是国际符号计算方面最强的研究群体之一,产生了领军人物、有基础意义的研究成果和软件,对整个科学界有很强的影响力”。
1992年参加在Berkeley举办的ISSAC后,我再次访问周咸青。周咸青此时在威奇托州立大学任教,而且张景中教授已先期到达。此后三年,我们三人合作研究几何定理机器证明的面积法,这一方法的起源是张景中教授为中学数学教学创立的基于面积的解题方法。面积法的主要想法是将吴先生工作中的变元消去法发展为基于几何不变量的几何定理证明方法,由此提高了机器证明的质量。这一工作得到包括图灵奖得主Dijkstra在内的广泛好评并于1997年由张景中院士领衔获得国家自然科学二等奖。
我于1996年回国,开始了在吴先生身边工作最长的一段时间。1997年,国家启动973项目。大家对数学机械化是否申请973项目一度犹豫不决,而程民德先生非常坚定地认为:数学机械化既是重大科学问题又有重要应用,符合“973”项目定位,应该积极申请。我记得最后的决定就是在程民德先生家中做出的。吴先生总结到“箭在弦上、不得不发”,我则代表课题组参加了答辩。经过激烈竞争,数学机械化入选国家首批“973”项目。在1997年秋天的评审中,共有270多个项目申请。经过三轮答辩,共评出15个项目,“数学机械化与自动推理平台”(1999-2003)为其中之一。按科技部的规定,吴先生因年龄原因不再担任首席科学家,改任项目学术指导,他建议我担任项目首席科学家。我记得他曾讲“谁说35岁不能做首席科学家。”此后15年里,我三次出任数学机械化方面973项目的首席科学家,这成为我一生非常珍贵的一段经历。我也没有辜负吴先生的信任,前两个973项目结题评估都在信息领域排名第一,第三个973项目虽然不知道排名,但也很成功,此文后面会提及。值得骄傲的是,前后参加攀登项目与973项目的郑志明、陈永川、王小云后来当选为中国科学院院士。
吴先生十分关心数学机械化研究与国家战略需求之间的联系,对现在说的“卡脖子”问题非常敏感。大约2007年秋天,吴先生在《参考消息》上看到一篇转自日本媒体的报道,其中讲到:虽然中国的经济发展很快,但是日本不必害怕。因为,很多核心的技术掌握在日本人手里。其中特别提到,中国还没有掌握高端数控的核心技术,因此中国高端制造业的发展将受制于他们。我记得非常清楚,在实验室的讨论班上,吴先生从他随身携带的一个黑色小书包中拿出这份报纸激动地对我们讲:“数学机械化方法有可能攻克这一关键技术,打破日本封锁。” 他希望我们尽快组织一个研究小组认真研究此事。2007年春节期间,吴先生又对前去看望他的路甬祥院长提及此事。路院长给詹文龙、阴和俊两位副院长写信,请他们组织数学机械化重点实验室与科学院有关单位合作,“凝聚若干优秀青年人员专心致志的工作,做出实实在在的成绩来。”2008年,科学院当时的基础局与高技术局设立联合项目,支持数学机械化重点实验室与中科院沈阳计算所开展数学机械化方法与高端数控技术的交叉研究。该项目结束后,国家科技部又设立了由我主持的973项目“数学机械化与数字化设计制造”(2010-2014),继续这一研究。我们没有辜负吴先生的期望,历经8年多的研究,在数控系统的核心技术“数控插补”方面提出了国际上最好的算法并在中科院沈阳计算所的商用数控系统中得到实现,显著提升了数控加工的精度与质量。
项目的成功与吴先生重视数学机械化的应用密切相关。吴先生对几何设计与机器人的研究影响深远,成了数学机械化应用研究的一个主要方向,国内外多支队伍从事这方面的研究,研究人员包括D. Kapur、C. Hoffmann、梁崇高、汪劲松、廖启征、刘慧林、陈发来等。我也在吴先生的影响下开始了这一方向的研究。数学机械化在开始阶段较多关注几何定理的机器证明。但工程领域很多问题往往可以归结为几何自动作图。例如,计算机辅助设计(CAD)被认为是信息时代最具影响的十项关键技术之一,实现几何自动作图是新一代智能CAD的核心算法。我提出了几何作图的高效方法,作为应用,引进了最一般的空间并联机构:广义Stewart平台,解决了具有优良运动学性质的并联机器人构型问题。Stewart平台有很多重要应用。例如,由国家天文台南仁东教授主持的FAST射电望远镜项目中用到了某种软性Stewart平台与刚性Stewart平台的耦合机构。我主持的“973”项目“数学机械化与自动推理平台”资助并承担了FAST射电望远镜馈源舱设计与控制的部分研究。
前面讲过,1985年春我在吴先生主持的讨论班上学习了Hodge和Pedoe的《代数几何方法》一书。本书以“周形式”为基础建立了相交理论。周形式在吴先生的数学机械化理论中也扮演了重要角色。周形式由华人数学家周炜良建立。吴先生多次给我们讲起周炜良的传奇经历。我的2007级研究生李伟选题时,我建议研究微分周形式,请李伟重读此书。这次是她讲我听。由此开始,我与李伟、袁春明合作建立了微分周形式理论与稀疏微分结式理论。其中关于稀疏微分结式的工作获得了国际计算机学会代数与符号计算专业委员会颁发的2011年ISSAC唯一杰出论文奖。当我将论文拿给吴先生时,他开玩笑说“我看不懂了”。但从他灿烂的笑容中,我可以看出他非常高兴。
2000年中科院推荐吴先生参加首届“最高科学技术奖”的评选。吴先生的申报材料由我与石赫为主整理。国家奖励办组织的首轮答辩由候选人单位介绍候选人的工作,吴的工作是我介绍的,记得汪成为先生是专家组组长。吴先生由于对拓扑学的基本贡献和开创了数学机械化研究领域毫无争议地获得首届国家最高科技奖。吴先生关于拓扑学的成果被5位菲尔兹奖得主引用,其中3位在其获奖工作中引用。有专家提问,为什么吴先生没有得奖?当时我可能没有回答好。多年后,在吴先生口述自传“走自己的路”中看到一些这个问题的线索。吴先生在拓扑方面最重要的工作是1950年做出的,而他1951年就回国了,使得若干已有的想法未能实现。书中提到,多位法国数学家讲过,如果1951年吴先生未回国,肯定能得菲尔兹奖。吴先生的工作还被多位诺贝尔奖得主引用。由于当年国内政治的影响,吴先生曾短暂从事过博弈论研究。他与学生江嘉禾先生合作于1962年发表了唯一一篇关于博弈论的研究论文,是迄今为止中国数学家在博弈论领域取得的最具国际影响的成就,被4位诺贝尔奖得主引用。虽然整个最高奖奖励申报过程吴先生参与不多,可以看出他很重视。有一次,他对我讲“此事很重要”。2001年3月29日中国科学院和国家自然科学基金委举办了“吴文俊先生荣获首届国家最高科学技术奖庆贺会暨数学机械化方法应用推广会”。石青云院士、金国藩院士、南仁东先生做报告介绍了数学机械化在他们领域的应用,我介绍了数学机械化中心的工作。2001年初,科技部推荐我参加国家在人民大会堂举办的元宵节联欢晚会。我想这有可能是对我在吴先生申报最高奖所做工作的一点奖励。
多年停顿后,中科院于2002年重新开始重点实验室的评审。数学机械化研究中心积极组织申请,并获得批准,吴先生任名誉主任,万哲先院士任学术委员会主任,我出任首届实验室主任。吴先生非常重视实验室的申请,我答辩时,他前来助阵。数学机械化重点实验室整合了数学机械化研究中心与万哲先院士建立的信息安全研究中心的力量,主要开展数学与计算机科学的交叉研究,在符号计算、自动推理、编码与密码学等领域具有重要的国际影响力。实验室现在由李洪波教授任主任、李邦河院士任学术委员会主任。
2006年,吴文俊与D.Mumford分享了当年的邵逸夫数学奖。有一天,我接到杨振宁先生的电话,问我吴先生在数学机械化方面有哪些专著,我介绍了吴先生的两本英文专著。评奖委员会及负责数学学科评选的Atiyah先生对吴先生在数学机械化方面的工作给予了高度评价,认为:“吴的方法使该领域发生了一次彻底的革命性变化,并推动了该领域研究方法的变革。通过引入深邃的数学想法,吴开辟了一种全新的方法。”其工作“揭示了数学的广度,为未来的数学家们树立了新的榜样。”这些评价对我来说多少有些在预料之中。在整理吴先生申报国家最高科技奖材料时,我就看到过一篇上世纪50年代Atiyah与Hirzebruch合作的论文,该论文基本上是在推广由吴先生证明的Cartarn公式。我想Atiyah从那时起就对吴先生留下了深刻印象吧。
吴先生在学术上的成功不是偶然的。他从事数学研究锲而不舍,终生努力,下死功夫。所以,他说过数学是“笨人”学的。吴先生年近花甲开始学习计算机编程,亲自上机编程验证他提出的机器证明方法。这可以说是一个奇迹,因为计算机编程一般被认为是非常繁重的工作,更适合青年人做。在此之前,由于没有计算机,他更是凭借坚强意志,手算上千项公式验证自己的方法。2009年,吴先生已经90岁高龄,却开始研究大整数分解这一世界级难题。大整数分解是当今使用最为广泛的密码的安全性的数学基础,受到广泛关注。我记得一次去看望吴先生,他很高兴地说,我发现了一个新的大整数分解算法,正在写程序验证其有效性,在计算机上分步计算,已经可以分解几十位的整数了。我当时很吃惊,因为此前从未听吴先生讲起他在思考这一问题。我也很感动,90岁高龄,吴先生仍在思考如此困难的问题,并且还自己在计算机上编程验证。我想这正是温家宝总理在纪念吴先生的文章中提到的吴先生一生“锲而不舍、积极进取”精神的真实写照。
2017年5月1日我去医院看望吴先生。当时吴先生正在休息,我没有打扰他。看护讲吴先生身体状况有很大改善,应该很快就能进行康复锻炼了。当时我心中还感到一丝宽慰。没想到,由于意外,吴先生病情急转直下于5月7日去世。回想自1984年考入吴先生门下学习30余年来的经历,浮现在我脑海中最多的是先生灿烂与慈祥的笑容,似乎在鼓励我继续努力工作。
仅以此文纪念吴先生百年诞辰。
2019年5月