尼克︱纪念数学家吴文俊先生：为人类文明做出贡献的中国人

吴文俊先生几天前（2017年5月7日）过世了，差几天就到他九十八岁生日。明天（5月13日）又是王浩逝世二十二年的纪念。吴先生长王先生两岁，两人都是五月来五月去。天才Wolfram有个习惯，每逢他敬仰的人的生日或辞世日，他都会在他博客上发文追思。王浩和吴文俊，他们的学问远超过我的智力所及，本没有资格怀念。今天写几段话讲讲王浩和吴文俊的交往。

吴文俊先生是数学家中的人精。“文革”前他就在关肇直影响下，研究应用问题，他最早和计算机相关的论文是讲怎么利用拓扑学给计算机电路布线的。“文革”期间他在北京无线电一厂下放，那是家计算机厂，他开始对计算机感兴趣。数学家学会了计算机编程，试试机器证明是最自然的。一开始的算法都是手工推演，1977年大年初一，吴文俊取得了突破。同年，他的文章“初等几何判定问题与机器证明”发表在《中国科学》上。吴文俊声称他的成果是在研究中国数学史时，受到启发。老一代人对中国传统的捍卫无法以理性解释。

哥德尔证明一阶整数（算术）是不可判定的，但塔尔斯基则证明一阶实数（初等几何和代数）是可判定的。塔尔斯基一直自认为他应该是和哥德尔比肩的逻辑学家。塔尔斯基的结果意味着可以存在算法能对所有初等几何和代数问题给出证明。塔尔斯基的原始算法是超指数的，在被后人多次改进之后仍然很难被当作通用算法。吴文俊的方法针对某一大类的初等几何问题给出了高效的算法。后来吴方法还被他推广到一类微分几何问题上。

周咸青（Chou Shang-ching）1978年在中科院研究生院旁听了吴文俊的几何定理证明的课，那时吴文俊的《几何定理机器证明的基本原理》还没正式出版，但周咸青已拿到书稿。他后来到德克萨斯大学奥斯丁分校留学，师从波尔（Boyer）和布莱索（Bledsoe），这两位虽都是逻辑系定理证明的大咖，但他们足够宽容，让周咸青对自己的博士论文题目自作主张，周的论文基本就是吴方法的实现。奥斯丁分校的硬件设备当然比吴文俊的环境好多了，周取得的成果自然也更加丰富。

王浩在得知吴文俊的结果后，于1978年4月10号给吴文俊写信。王浩建议吴文俊利用已有的代数包，甚至考虑自己亲自动手写个程序实现吴的方法。王浩和吴文俊的通信大概是哥德尔系定理证明和塔尔斯基系定理证明为数不多的交流。

基于逻辑的定理证明器最适合解决代数问题，而几何定理证明器却又都是基于代数的。王浩是逻辑系定理证明的先驱，吴文俊则开几何系定理证明的风气之先。哥德尔定理和塔尔斯基定理在人工智能问题上各有蕴意，是为后话。有意思的是塔尔斯基对机器定理证明的结果不感兴趣。

1979年吴文俊的工作得到杨振宁的关注，当时的科学院副院长李昌和刚成立的科学院系统所所长关肇直都大力支持吴文俊，并为他申请到两万美元去美国购买一台家用电脑，以实现他的吴方法。吴文俊到美国的重要一站是去洛克菲勒大学会见王浩。吴文俊的工作在定理证明界迅速引起重视，王浩起了关键的推动作用。吴文俊1997年获得第四届Herbrand奖，这是定理证明领域的最高奖项。在他前面获奖的有沃思（Wos）、布莱索和发明归结算法的罗宾逊（Robinson），马丁·戴维斯迟至2005年才获奖。

吴文俊的长寿也体现在他的学术生命。1979年吴文俊六十高龄开始学习计算机编程语言，先是BASIC，后又Algol，再后又Fortran。他在那台两万美元的家用电脑上不断取得新的成果。后来系统所的硬件设施改进，吴文俊在相当一段时间里都是上机时间最长的。

物理学怪才兼企业家弗里德金（Edward Fredkin）曾为计算机下棋设立过奖项。但不大为人所知的是他为机器定理证明也设立过一个奖项，分三等，第三等是当前成果奖（Current），1983年沃思和温克获奖，1991年波尔和摩尔获奖。二等奖是里程碑奖，1983年给了王浩，1984年给了罗宾逊，1991年给了布莱索。一等奖被称为莱布尼茨奖（注意：和德国的那个莱布尼茨奖不同），一次也没发出过，因为条件是“不仅够格在数学杂志上发表，还要够格评选美国数学会的Cole奖或Veblen奖，甚至菲尔茨奖”。弗里德金为计算机下棋设定的几个奖项有明确的标准：战胜特级大师，战胜当前世界冠军。按此标准就不难理解为什么马库恩（McCune）的罗宾斯猜想的机器证明尚不够格一等奖。马库恩的前老板、定理证明的领袖人物沃思（Larry Wos）认为马库恩应该很接近了。但该奖的评委、哈佛数学家大卫·芒福德（David Mumford）想都不想地说：“现在不行，一百年都够呛（Not now, not 100 years from now）。”随着定理证明事业的凋零，该奖后来也悄无声息地撤销了。也有乐观派：离散数学家格雷汉姆（Ron Graham ，他的太太是另一位成果丰富的离散数学家Fan Chung金芳蓉）认为在证明定理上计算机超过人是迟早的事，人脑毕竟是生物进化的产物，天生的目的不是用来证明定理的。

吴文俊的哲学思想是典型的数学家思路，这和逻辑学家不尽相同。吴老一次讲座中讲计算机和数学机械化，引用维纳的说法：“人脑贬值，至少人脑所起的较简单、较具常规性质的判断作用，将贬值。”笛卡儿认为代数使得数学机械化，因而使得思考和计算步骤变得容易，无需花很大脑力。小学算术很难的东西，初中代数立个方程马上就解了。每一次数学的突破，往往以脑力劳动的机械化体现。我想吴老应该算乐观派。

杨振宁曾说他自己最重要的成就是提高了中国人的自信。陈省身、华罗庚、杨振宁、李政道那一批人是最早为人类文明做出点贡献的中国人。我想那个不长的名单里还应该有王浩和吴文俊。