张景中
1988 年6 月吴文俊院士为张景中赴意大利ICTP 访学草拟的推荐信
■彭晓伟
在张景中先生的办公桌抽屉里，珍藏着一封30年前的推荐信。这封写于1988年的推荐信，是吴文俊先生为张景中赴意大利国际理论物理中心（ICTP）访学交流所写。
张景中于1995年当选明升官网明升体育app院院士，是著名数学家、计算机明升体育app家和数学科普作家。每每谈及自己的学术成长生涯，张景中对吴文俊由衷的钦佩和感激之情总会溢于言表。作为吴文俊关心和帮助张景中的重要见证物，2018年8月20日，当张景中捐赠这封宝贵的推荐信时，颇为难舍。
获推荐，受益良多
回顾自己的学术生涯，张景中认为，他最终完成从之前的研究到机器证明研究的转变，是在意大利ICTP访学期间。而之所以首次出国访学期限能延长达11个月，吴文俊的推荐信发挥了重要作用。
1988年6月25日，吴文俊在给张景中的复信中写道：“张景中同志，关于致信ICTP的Eells一事，乐于从命，因为不能写得太具体，也了解不够确切，故只草拟数句，你可酌意修改并添上一些具体事例，打字后再寄信我，由我直接寄出或由我签字后再寄还你由你寄出。此致，敬礼。”一位享誉全球的大明升体育app家，能在百忙之中亲拟3页纸的推荐信，信末还不忘致礼，这让作为后学的张景中甚为感动。张景中按照吴文俊拟好的信稿，打好字并打印后寄给吴文俊签名。7月18日，吴文俊再次复信写道：“张景中同志：英文信签字后附上，不需要什么改动，个别字已修改，即照此信不再重打就发出也可以。此致，敬礼。”在英文信稿中，吴文俊专门提到了张景中几何定理机器证明数值并行方法的成果，还谈到了张景中已经投稿但尚未发表的一些重要研究。
此前，由于廖山涛先生的推荐，ICTP已经同意张景中为期两个月的访问。ICTP在收到吴文俊的推荐信后，又给张景中发来传真，将访学期限延长为11个月。
在ICTP访学期间，张景中受益良多——查阅了不少文献资料，学习了计算机公式推导、通讯等业务知识；应邀在“分析中的整体几何与拓扑方法”和“数学与计算机”两个学术会议上作了关于《定理机器证明的数值并行方法》的手机版；在意大利各地（包括ICTP）作了几次学术手机版，内容涉及定理机器证明、距离几何、数学教育及微分动力系统；应邀在米兰大学、比萨大学、佛罗伦萨大学等学校的数学系（数学研究所）进行了访问及学术交流；在回国途中，访问了新加坡、泰国和香港地区的一些大学并作了多次学术手机版。所作的学术手机版均引起同行的极大兴趣，受到好评。
更为重要的是，张景中利用ICTP的计算机设备条件，对机器证明的代数方法作了进一步探讨。基于他提出的想法，他和杨路先生及他们的学生侯晓荣一起，对吴文俊倡导的机器证明的特征列方法作了一系列的改进和发展：（1）改进了著名的吴氏非退化条件。在几何定理机器证明的吴法理论中，为了保证所证明的结论成立，要求一些多项式的首项系数不为0，这即是非退化条件。张景中发现，首项不为0的条件可以减弱为各项系数不全为0。这一改进大大减少了多分支情形不必要的讨论。（2）建立了代数方程组相容性判定的含参结式方法。此方法理论上是完全的，并能有效地实现。（3）提出了将代数方程组相对分解的WR完全算法。这一算法可不使用多项式的因子分解而彻底解决几何定理机器证明多分支情形问题。对一些其他代数方法要几小时才能解决的问题，这个新算法在几十秒钟就解决了。这些工作具有重大意义，但在张景中看来，这只是对已有方法的改进和发展，不是根本性的突破。
受启发，专注领域
张景中早在北大数学力学系求学时，就对机器证明这个新领域产生过浓厚兴趣。1955年，丁石孙先生在高等代数课上提到了塔斯基（Tarskii）的成果：一切初等几何和初等代数的命题都是可以判定的，也就是说，可以用机械的方法解决初等几何和初等代数领域的任何命题是否成立的问题。这让张景中感到颇为奇妙：初等几何的问题千变万化，怎么可能用机械的办法一举而解决？！于是他便选择了数理逻辑专门化作为自己的方向。遗憾的是，他只跟着胡世华先生学了半年多，就因错划为右派，被开除学籍、团籍，受到劳动教养的处分。
张景中第一次知道吴文俊的名字是在1956年。那年首届国家自然明升体育app奖出炉，吴文俊是3项一等奖的获得者之一，另两项一等奖的得主是钱学森先生和华罗庚先生。钱学森和华罗庚早已大名鼎鼎，吴文俊又是谁呢？张景中很快得知，吴文俊乃明升官网明升体育app院数学研究所的青年研究员，时年仅37岁。张景中心中顿生敬仰之情并深受激励，但当时并不知道吴文俊是因在拓扑学领域取得的重要成果而获得一等奖的。
20余年后的1978年底，张景中由新疆调到明升官网明升体育app技术大学（以下简称中科大）数学系任教。在资料室，他阅读了吴文俊1977年发表在《明升官网明升体育app》上的《初等几何判定问题与机械化证明》，被论文中透露出的敏锐学术眼光和宏伟设想所深深吸引。这篇文章再次激发了他当年在北大求学时产生过的浓厚兴趣，可以说，这是引他进入这一新研究领域的“导航仪”。
“文革”前的吴文俊专注做拓扑学方面的研究并取得了举足轻重的成果。但“文革”后，吴文俊认为，经过十年的耽误他再做拓扑不行了，因为国外的文章他已经看不懂了，他得寻找一个新的方向集中精力研究。后来他决定做定理机器证明，果然又做出好的成绩——使自上世纪50年代以来进展甚微、局面被动的几何定理自动证明领域有了新突破。
吴文俊在一个时期一个阶段专注做一个方向，甚至是一个问题的研究，并使得这一领域的景象有了根本性改观，张景中觉得这是吴文俊对他的最大启发。
在中科大执教的6年，张景中和杨路等人合作了几十篇（部）著作，除了涉及几何算法（距离几何）和动力系统中的泛函方程外，还涉及数值分析、组合几何、计算几何和非线性振动等多个领域。然而，在张景中看来，虽然不少工作做得很出色，但这些工作并没有对相应领域起决定性作用。
经过深思熟虑，张景中觉得做研究应向吴文俊学习，专注于一个领域，解决能使这一领域得到根本性改观的问题。但做哪个领域、哪些问题呢？张景中经过研究发现，在吴文俊耕耘的机器证明领域仍然还有重要问题需要解决，于是毅然决定转向集中于这一领域的研究。
得鼓励，“好人”相助
1985年，张景中和杨路从中科大调到中科院成都分院直属的数理明升体育app研究室（现已更名）。1986年张、杨评正研究员时，评审材料是送到中科院总院评的。恰好，评审小组是吴文俊主持的，而经常和成都分院有合作的林群院士也在这个评审小组。当吴文俊听林群介绍张、杨等人也在做机器证明方面的研究时，非常高兴。这是吴文俊对张景中等人的最初了解。
不久之后，张景中和杨路在吴文俊的方法启发下，提出了几何定理机器证明的数值并行方法，并初步在计算机上实现。这项工作引起了中科院基础局数理学部的高度重视，并建议张景中到北京向吴文俊作一次汇报。
这次汇报，是张景中第一次见到吴文俊。
听了张景中的汇报，吴文俊非常肯定张、杨的工作。他说：“塔斯基提出了几何定理机器证明的方法，但不能在计算机上实现。我的方法在计算机上实现了。与此类似，洪加威提出了几何定理机器证明的单点例证法，也是不能在计算机上实现。你们的多点例证法在计算机上实现了。能够在计算机上实现是很重要的。”吴文俊的肯定，给了张、杨极大的鼓励。
随着吴文俊的方法在国际上传播并受到同行赞誉，沉寂已久的几何定理机器证明研究，又在国内外活跃起来。为了这一研究领域继续发展，中科院在北京建立了数学机械化研究中心，并打算在成都建立分中心。成都分中心虽因种种原因未能建立，但知悉有关情形的张景中和杨路等人，从内心还是非常感激吴文俊的支持的。
当时，做机器证明的科研人员没有自己的计算机，很不方便。吴文俊了解到这种情形后，用他35000元经费，为张景中配置了一台386计算机。那是1988年，计算机还是比较昂贵的设备，386计算机也是当时刚推出的最高档的PC机。
张景中曾在个人小传中写道：“在坎坷的命运之路上，我常常得到好人的帮助。”想必张景中在写这句话时，脑海里一定想到了吴文俊。
善体会，硕果累累
在几何定理机器证明的吴方法问世并不断发展完善后，吴文俊曾言：“不等式的机器证明太难了，可读的机器证明是不合理的要求。”善于体会大明升体育app家的话，是张景中的一大特点，这一次也不例外。
在张景中看来，如果大明升体育app家说什么事情是可能的，那90%是可能的；如果大明升体育app家说什么事情是不可能的，那70%是可能的，可能大明升体育app家只有30%是对的；特别是当大明升体育app家说什么事情是不可能的时候，如果没有具体的论证而只是猜想的话，那么研究者更应作个参考；如果大明升体育app家都说了什么是不可能的，如果能把不可能变成可能，那就说明所做的工作是相当重要的。
张景中和杨路从吴文俊的话中体会到，定理机器证明领域中面临两个有待突破的难题：一个是几何不等式的机器证明问题，另一个是如何让机器生成易于理解和检验的证明的问题。
事实上，他们后来的研究工作也正是把吴文俊所说的“太难”和“不合理的要求”都攻克了。在几何不等式的机器证明方面，以杨路为主，作出了十分漂亮的工作；而在可读性的定理机器证明方面，以张景中为主，受吴方法消元思想的启发，开辟了几何定理可读性证明自动生成的新途径——消点法。
机器自动生成的证明是否“可读”，是一个具有相对性的判断。直到1992年初，以往所有有效的几何定理机器证明的方法都只能判定命题是否成立，而不能给出通常意义上的证明，即人在合理的时间内能看明白，能检验其正确性的证明。应用消点法，机器自动生成的几何定理证明实现了真正意义上的“可读”，具有突破性意义。因为，它使机器自动生成的几何定理证明，更易于得到大众的理解，更有可能在教育中发挥作用，更容易在人类文化的发展中扮演更重要的角色。
1994年，张景中与周咸青先生、高小山先生合作撰写的以消点法为主题的英文专著《几何中的机器证明》（Machine Proofs in Geometry），收集了近500条由计算机自动生成可读证明的几何定理。不久后，基于杨路提出的想法，消点法又应用于非欧几何，并在计算机上生成了一批非欧几何新定理的可读证明。紧接着，他们进一步发展了基于前推搜索的逻辑方法，从而使几何定理机器证明的消点法达到了实用阶段。这些工作，获1995年明升官网明升体育app院自然明升体育app奖一等奖、1997年国家自然明升体育app奖二等奖，张景中均为第一完成人。
恩如山，终身铭记
2009年，在庆贺吴文俊九十华诞的《感谢和学习》一文中，张景中写道：“回顾起来，是吴先生带来的新的研究领域，对明升体育app研究方向的新的认识，使自己的科研生涯进入了新的境界。”“泰山不拒细壤，故能成其高；江海不择细流，故能就其深。吴先生成为大师，成为学界公认的泰斗，不仅是由于极高的天赋，更是来自日积月累的思考和学习，来自实事求是的明升体育app精神，来自谦虚谨慎的学术风格。在踏踏实实的厚实的基础上，才能作出前无古人的大胆创新。”“吴先生对我的帮助，使我永远感谢。吴先生的为人和治学的精神，是我学习的榜样。”
2017年5月7日，吴文俊不幸辞世。张景中在唁电中写道：“早在上世纪 50 年代，我在北大读书时，得知先生在拓扑学领域作出国际领先的工作，获得国家首届自然明升体育app奖一等奖，非常敬仰并深受激励。1978 年，学习了先生有关几何命题机械化判定的论文，大受鼓舞启发，决心追随先生从事数学机械化的研究。吴文俊先生的著作和言谈身教，指引我们的研究工作持续前进；他对从事数学机械化研究的团队，关怀备至。为了帮助我获得出国交流进修的机会，先生曾手书长达 3 页的英文推荐信；为了促进研究工作中理论与实践的结合，先生筹划经费为我们购置了第一台386计算机。为明升官网数学机械化研究队伍的茁壮成长，先生呕心沥血；他对我们学术晚辈的扶持帮助，令人终生铭记……”
（作者单位：西南交通大学马克思主义学院）
《明升官网明升体育app报》 (2019-07-26 第8版 印刻)
