一封珍藏了三十年的推荐信(3)

不久之后，张景中和杨路在吴文俊的方法启发下，提出了几何定理机器证明的数值并行方法，并初步在计算机上实现。这项工作引起了中科院基础局数理学部的高度重视，并建议张景中到北京向吴文俊作一次汇报。

这次汇报，是张景中第一次见到吴文俊。

听了张景中的汇报，吴文俊非常肯定张、杨的工作。他说：“塔斯基提出了几何定理机器证明的方法，但不能在计算机上实现。我的方法在计算机上实现了。与此类似，洪加威提出了几何定理机器证明的单点例证法，也是不能在计算机上实现。你们的多点例证法在计算机上实现了。能够在计算机上实现是很重要的。”吴文俊的肯定，给了张、杨极大的鼓励。

随着吴文俊的方法在国际上传播并受到同行赞誉，沉寂已久的几何定理机器证明研究，又在国内外活跃起来。为了这一研究领域继续发展，中科院在北京建立了数学机械化研究中心，并打算在成都建立分中心。成都分中心虽因种种原因未能建立，但知悉有关情形的张景中和杨路等人，从内心还是非常感激吴文俊的支持的。

当时，做机器证明的科研人员没有自己的计算机，很不方便。吴文俊了解到这种情形后，用他35000元经费，为张景中配置了一台386计算机。那是1988年，计算机还是比较昂贵的设备，386计算机也是当时刚推出的最高档的PC机。

张景中曾在个人小传中写道：“在坎坷的命运之路上，我常常得到好人的帮助。”想必张景中在写这句话时，脑海里一定想到了吴文俊。

善体会，硕果累累

在几何定理机器证明的吴方法问世并不断发展完善后，吴文俊曾言：“不等式的机器证明太难了，可读的机器证明是不合理的要求。”善于体会大科学家的话，是张景中的一大特点，这一次也不例外。

在张景中看来，如果大科学家说什么事情是可能的，那90%是可能的；如果大科学家说什么事情是不可能的，那70%是可能的，可能大科学家只有30%是对的；特别是当大科学家说什么事情是不可能的时候，如果没有具体的论证而只是猜想的话，那么研究者更应作个参考；如果大科学家都说了什么是不可能的，如果能把不可能变成可能，那就说明所做的工作是相当重要的。

张景中和杨路从吴文俊的话中体会到，定理机器证明领域中面临两个有待突破的难题：一个是几何不等式的机器证明问题，另一个是如何让机器生成易于理解和检验的证明的问题。

事实上，他们后来的研究工作也正是把吴文俊所说的“太难”和“不合理的要求”都攻克了。在几何不等式的机器证明方面，以杨路为主，作出了十分漂亮的工作；而在可读性的定理机器证明方面，以张景中为主，受吴方法消元思想的启发，开辟了几何定理可读性证明自动生成的新途径——消点法。

机器自动生成的证明是否“可读”，是一个具有相对性的判断。直到1992年初，以往所有有效的几何定理机器证明的方法都只能判定命题是否成立，而不能给出通常意义上的证明，即人在合理的时间内能看明白，能检验其正确性的证明。应用消点法，机器自动生成的几何定理证明实现了真正意义上的“可读”，具有突破性意义。因为，它使机器自动生成的几何定理证明，更易于得到大众的理解，更有可能在教育中发挥作用，更容易在人类文化的发展中扮演更重要的角色。