来源：图灵社区

作者：林军 岑峰

工作中的吴文俊（1919年5月12日－2017年5月7日）。图源：中国科学院数学与系统科学研究院

1979 年在中国是一个重要的年份。这一年发生了诸多大事，也被视为中国在政治、经济、科技、 文化等多个领域的一个重要转折点和中国近现代历史重要的时期断代点之一。相比1979 年所开启的波澜壮阔的新时代，中国人工智能(Artificial Intelligence，AI)研究在1979 年的起步只能算历史大潮中的一朵不起眼的浪花，但在中国人工智能的历史里，这是开天辟地的大事件。

人工智能最早的学派是符号主义学派，最早一批人工智能科学家多半是数学家和逻辑学家，他们在计算机诞生后把计算机与自己的研究结合起来，从而进入人工智能领域。在中国，同样是由数 学家翻开了人工智能研究的第一页。在1979 年，无论是机器证明中的“吴方法”走向世界，还是堪比达特茅斯会议的计算机科学暑期讨论会的举办，其背后都有着数学家的身影。也正是从这一年起，中国人工智能迈开了追赶世界的脚步。

“吴方法”的提出者，正是数学家吴文俊。他与王湘浩、曾宪昌并称“机器证明三杰”。1970年代后期，近花甲之年的吴文俊从研究中国古代数学出发，开创了崭新的数学机械化领域，提出了用计算机证明几何定理的“吴方法”，被认为是自动推理领域的先驱性工作。

一、吴文俊推开了中国人工智能走向世界的大门

1979 年 1 月，应普林斯顿高等研究院的邀请，数学家吴文俊怀揣 2.5 万美元，登上了赴美交流的班机。

与他同行的是数学家陈景润。二人是中美正式建交后第一批应邀赴美学习访问的科学家，将在普林斯顿高等研究院学习和交流一段时间。陈景润交流的主题自然是 “1+2”，而吴文俊此行交流的主要内容，除了他的老本行拓扑学，更多的是中国古代数学史和数学机械化，他想用自己携带的 2.5 万美元购买一台计算机，用于数学机械化的研究。

吴文俊在1979 年获得中国科学院(下称“中科院”)自然科学一等奖时，数学机械化已经成为他的主要研究方向。这个研究方向也受到世人瞩目，吴文俊的研究方法在机器定理证明界被称为“吴方法”，中国智能科学技术最高奖“吴文俊人工智能科学技术奖”就使用了吴文俊的名字，以纪念吴文俊作为中国研究者在人工智能相关领域取得的成就。

不经意间，吴文俊推开了中国人工智能研究走向世界的大门。吴文俊对中国古代数学史的研究始于 1974 年前后。当时中国科学院数学研究所(下称“中科院数学研究所”)副所长关肇直让吴文俊研究中国古代数学。吴文俊很快发现了中国古代数学传统与由古希腊延续下来的近现代西方数学传统的重要区别，对中国古代算术进行了正本清源的分析，在许多方面产生了独到的见解。

20 世纪 70 年代，对外学术交流开始逐步恢复。1975 年，吴文俊赴法交流，并在法国高等科学研究所作了关于中国古代数学思想的报告。这时吴文俊已经复原了日高公式的古代证明，并注意到了中国古代数学的“构造性”和“机械化”的特点。1977 年春节，吴文俊用手算验证了几何定理机器证明方法的可行性，这一过程历时两个月。

机器定理证明最初的思想源自戈特弗里德·威廉·莱布尼茨(Gottfried Wilhelm Leibniz)的演算推论器，以及之后演化而来的符号逻辑。后来，戴维·希尔伯特 (David Hilbert)在此基础上于 1920 年推出了“希尔伯特计划”，希望将整个数学体系严格公理化。简单来讲，如果这一计划实现，就意味着对于任何一个数学猜想，不管它有多难，我们总能够知道这个猜想是否正确，并且证明或否定它。希尔伯特说的“Wir müssen wissen,wir werden wissen”(我们必须知道，我们必将知道)便是这个意思。

然而，就在此后不久的 1931 年，库尔特·哥德尔(Kurt Gödel)就提出了哥德尔不完备定理，彻底粉碎了希尔伯特的形式主义理想。但不管怎么说，哥德尔在关上这扇门的时候还是留了一扇窗。法国天才数学家雅克·埃尔布朗(Jacques Herbrand) 的博士论文为数理逻辑的证明论和递归论奠定了基础，埃尔布朗在哥德尔不完备定理被提出后，检查了自己的论文，留下一句话——哥德尔和我的结果并不矛盾，并向哥德尔写了一封信请教。哥德尔回复了埃尔布朗，但埃尔布朗没能等到这封信，他在哥德尔回信两天后死于登山事故，年仅 23 岁。后来，定理证明领域的最高奖项也以埃尔布朗的名字命名，吴文俊在 1997 年获得了第四届埃尔布朗自动推理杰出成就奖。

其他数学家对哥德尔定理也进行了补充。就在哥德尔证明“一阶整数(算术)是不可判定的”之后不久，阿尔弗莱德·塔尔斯基(Alfred Tarski)证明了“一阶实数(几何与代数)是可以判定的”，这也为机器证明奠定了基础。

1936 年，图灵在他的重要论文《论可计算数及其在判定问题上的应用》(On Computable Numbers, with an Application to the Entscheidungsproblem)中对哥德尔在 1931 年证明和计算限制的结果重新进行了论述，并用现在叫作图灵机的简单形式的抽象装置代替了哥德尔的以通用算术为基础的形式语言，证明了一切可计算过程都可以用图灵机模拟。这也是计算机科学和人工智能的重要理论基础。人工智能最早的学派——符号学派也正是在形式逻辑运算的基础上延伸而来的。

回过头来说吴文俊，他在 20 世纪 70 年代到生产计算机的北京无线电一厂工作， 并在那个时候开始接触计算机和机器定理证明。“如何发挥计算机的威力，将其应用到自己的数学研究上”成为吴文俊感兴趣的内容。后来，吴文俊开始研究中国古代数学史，并总结出中国古代数学的几何代数化倾向和算法化思想。在发现中国古代数学与西方数学的不同思路后，他决定换一种方法来做几何定理的机器证明。

那个时候，吴文俊阅读了很多国外的文章，充分了解了机器证明。当时，机器定理证明最前沿的研究来自数理逻辑学家王浩，他在西南联大数学系读书期间曾师从著名哲学家、“中国哲学界第一人”金岳霖，后前往美国哈佛大学，在著名哲学家、逻辑学家威拉德·冯·奎因(W. V. Quine)门下学习奎因创立的形式公理系统并获得博士学位。早在1953 年，王浩就已经开始思考用机器证明数学定理的可能性了。

1958 年，王浩在一台 IBM 7041 计算机上使用命题逻辑程序证明了《数学原理》中所有的一阶逻辑定理，次年又完成了全部 200 条命题逻辑定理的证明。王浩之工作的意义在于宣告了用计算机进行定理证明的可能性。他在 1977 年回国时参加了多个影响我国科技长远发展的讨论会，并在中科院作了 6 次专题演讲，对国内机器证明研究有着重大的影响。

言归正传，王浩此前对《数学原理》中命题逻辑定理的证明和吴文俊想要实现的几何定理机器证明之间还存在着鸿沟，前者符号逻辑的成分更多，后者则有推理的成分在内。当时，国外有很多对几何定理机器证明的研究，但都以失败告终。

二、从中国古代数学思想的机械化到“吴方法”

在吴文俊看来，失败的经验也是很重要的，它会告诉你哪些路是走不通的。他受笛卡儿思想的启发，通过引入坐标，把几何问题转化为代数问题，再按中国古代数学思想把它机械化了。吴文俊甚至把笛卡儿思想与中国古代数学思想结合起来，提出一个解决一般问题的路线：

所有的问题都可以转变成数学问题，所有的数学问题都可以转变成代数问题，所有的代数问题都可以转变成解方程组的问题，所有解方程组的问题都可以转变成解单变元的代数方程问题。

中国古代数学与西方的现代数学是两套不同的体系。吴文俊在不借助现代数学中的三角函数、微积分、因式分解法、高次方程解法等“现代工具”的情况下，按古人当时的知识和惯用的思维推理复原了《周髀算经》《数书九章》中的“日高图说”“大衍求一术”“增乘开方术”的证明方法。他认为中国古代数学有着自己的独到之处，秦九韶的方法具有构造性和可机械化的特点，用小计算器即可求出高次代数方程的数值解。在当时缺乏高性能计算设备的情况下，吴文俊能充分利用中国古代数学思想降维进行研究，也是难能可贵的事情。

吴文俊按照这一思路证明的第一个定理是费尔巴哈定理，即证明了“三角形的九点圆与其内切圆以及三个旁切圆相切”。这是平面几何学中十分优美的定理之一，吴文俊的审美可见一斑。当时没有计算机，吴文俊就自己用手算。“吴方法”的一个特点是会产生大量的多项式，证明过程中涉及的最大多项式有数百项，这一计算非常困难，任何一步出错都会导致后面的计算失败。1977年春节，吴文俊首次用手算成功验证了几何定理机器证明的方法，后来，吴文俊又在一台由北京无线电一厂生产的长城203上证明了西姆森定理。

吴文俊将相关的研究文章《初等几何判定问题与机械化证明》发表在 1977 年的《中国科学》上，并将文章寄给了王浩。王浩高度评价了吴文俊的工作，并复信建议吴文俊利用已有的代数包，考虑用计算机实现吴方法。王浩没有意识到这个时候中美两国最顶尖的学者所使用的计算机的差别：长城 203 可以使用机器语言，但不同计算机的指令系统并不通用，利用已有的代数包行不通。所以，后来吴文俊干脆从中科院数学研究所里借了一台来中科院数学研究所访问的外国人赠送的小计算器，把所给命题转化为代数形式，再用秦九韶的方法来计算高阶方程的解。

吴文俊几何定理机器证明的研究得到了关肇直的大力支持。关肇直曾在法国留学，是中国科学工作者协会旅法分会的创办人之一，团结了一批优秀的爱国知识分子，吴文俊就是其中之一。当时，吴文俊所在的中科院数学研究所关系复杂，有一派认为做机器证明是“离经叛道”，希望他继续从事拓扑学研究；从拓扑学和泛函分析转入控制理论的关肇直却格外支持和理解他，放话说吴文俊想干什么就让他干什么。后来，关肇直在1979 年“另立山头”，成立中科院系统科学研究所时，吴文俊也跟随关肇直到了中科院系统科学研究所(图1-1)。

图 1-1 20 世纪 80 年代初中科院系统科学研究所原办公楼(现融科大厦) (左起：许国志、吴文俊、印度学者、关肇直)

要证明更复杂的定理，需要有更好的机器。时任中科院声学研究所所长的汪德昭院士指点了吴文俊。他告诉吴文俊中科院党组书记、副院长李昌何时何地会出现，结果真被吴文俊守到了。李昌非常开明，在 20 世纪 50 年代担任哈尔滨工业大学(下称“哈工大”)校长期间把哈工大办成了全国一流大学。在 1954 年确定的全国六所重点大学中，哈工大是唯一一所不在北京的大学。李昌对吴文俊的工作同样给予了很大支持，吴文俊去美国买计算机的 2.5 万美元外汇就是由李昌特批的。有了这台计算机，很多定理很快被证明出来了。

20 世纪 70 年代也是机器定理证明的黄金时代。1976 年，两位美国数学家用高速电子计算机耗费 1200 小时的计算时间证明了四色定理，数学家们 100 多年来未能解决的难题得到解决。四色定理之所以能被证明，是因为不可约集和不可避免集是有限的，四色定理的“地图涂色”问题看似有无穷多的地图，实际上可以把它们归结为 2000 多种基本形状，之后利用计算机的计算能力暴力穷举，一个个去证明即可。打个比方，这种方法如同复原魔方——将魔方拆散并重新拼好——虽不优雅但确实有效。我们现在说GPT-3“大力出奇迹”，其实四色定理的证明才是“大力出奇迹”的始祖。

然而，这种利用计算机计算能力暴力破解定理证明的做法并不能得到推广。定理证明的第一步，即定理的形式化，需要完整和严谨的表述。关于这一点，有一个关于数学家的小故事。一个天文学家、一个物理学家和一个数学家乘坐火车到苏格兰旅行，他们看到窗外有一只黑色的羊，天文学家开始感慨：“怎么苏格兰的羊都是黑色的？”物理学家纠正：“应该说苏格兰的一些羊是黑色的。”而最严谨的表达则来自数学家：“在苏格兰至少存在着一块天地，至少有一只羊，这只羊至少有一侧是黑色的。”还有一个段子，说数学问题分两类：一类是“这也要证？”，一类是“这也能证？”。由此可知，一个证明要得到其他数学家的认可是多么不容易。同样，要在一个交互式定理证明器里形式化一个定理，需要填补所有的技术细节，才能完成推理的“自动化”，最终用一种可行但是计算量很大的解题思路来代替对定理的证明。换言之，这种方式仍然依赖数学家对定理的理解，只能做到“一理一证”，只能算定理的计算机辅助证明。

所以，在四色定理被计算机证明后，包括王浩在内的一批逻辑学家提出了不同意见：四色定理算被证明了吗？这种证明方式算传统证明，计算机只是起到了辅助计算的作用。一直到 2005 年，乔治·贡蒂尔(Georges Gonthier) 才完成了四色定理的全部计算机化证明，其每一步逻辑推导都是由计算机完成的。目前人们已经用计算机证明了数百条数学定理，但这些定理大多是已知的，“机器智能”还未对数学有真正意义上的贡献。

机器定理证明依赖于算法。在早期阶段，研究者们往往试图找到一个超级算法去解决所有问题，而吴文俊则将中国古代数学思想应用于几何定理的机器证明领域，做到了“一类一证”。这一点也得到了王浩的赞同，他认为自己的早期工作和吴文俊使用的方法具有共同点，即先找到一个相对可控的子领域，然后根据这个子领域的特点找出最有效的算法。吴文俊在 1979 年访美的时候还特地去洛克菲勒大学拜访了王浩，他的工作在机器定理界受到重视也和王浩的力荐有着一定的关系。

“吴方法”真正传播开来，让机器定理证明在 20 世纪 80 年代第一次取得突破性进展，还有赖于曾经听过吴文俊机器定理证明课程的一位在美留学生——周咸青。周咸青本想考吴文俊机器证明方向的研究生，不过他认为微分几何是自己的弱项，害怕考不上，最终考到中国科学技术大学(下称“中科大”)，后来到中科院计算技术研究所代培，就此旁听了吴文俊的几何证明的课程。

1981 年，周咸青到得克萨斯大学奥斯汀分校留学，当时得克萨斯大学奥斯汀分校堪称定理证明界的王者，该校的两个研究小组都曾获得定理证明的最高奖赫布兰德奖。周咸青向罗伯特·博耶(Robert Boyer)提及了吴文俊的工作，博耶觉得很新鲜，便继续追问，但周咸青只知道是将几何转化为代数，具体细节则讲不出所以然。

之后，伍迪·布莱索(Woody Bledsoe)便让周咸青和另一位学生王铁城去搜集资料，周咸青的博士论文便是吴方法的实现。吴文俊很快寄来了两篇文章，文章上都有他给布莱索的签名。在此后两年，这两篇文章被得克萨斯大学奥斯汀分校复印了近百次寄往世界各地，吴方法开始广为人知。

1983 年，全美定理机器证明学术会议在美国科罗拉多州举行，周咸青在会议上作了题为“用吴方法证明几何定理”的报告。周咸青开发的通用程序能自动证明 130 多条几何定理，其中包含莫勒定理、西姆森定理、费尔巴哈九点圆定理和笛沙格定理等难度较大的定理的证明。之后，这次会议的论文集作为美国《当代数学》系列丛书第 29 卷于1984 年正式发表，吴文俊寄来的两篇相关论文也被收录其中。

1986 年 6 月，图灵奖获得者约翰·霍普克罗夫特(John Hopcroft)等人组织了一场几何自动推理的研讨会，讨论会的部分报告被收录在 1988 年 12 月的《人工智能》 特辑中，特辑的引言文章特别介绍了吴文俊提出的代数几何新方法，认为该方法不仅为几何推理的进步做出了巨大贡献，在人工智能的三大应用问题（机器人和运动规划、机器视觉、实体建模）中也都具有重要的应用价值(图1-2)。霍普克罗夫特此后与中国多所高校密切合作，在上海交通大学、北京大学、香港中文大学(深圳)均有由他牵头的研究机构，吴文俊和吴方法大概就是他有中国情结的开始。

图 1-2 1988 年《人工智能》特辑开篇对吴方法的概述