1979年在中国是一个重要的年份。这一年发生了诸多大事,也被视为中国在政治、经济、科技、文化等多个领域的一个重要转折点和中国近现代历史重要的时期断代点之一。相比1979年所开启的波澜壮阔的新时代,中国人工智能(Artificial Intelligence,AI)研究在1979年的起步只能算历史大潮中的一朵不起眼的浪花,但在中国人工智能的历史里,这是开天辟地的大事件。
人工智能最早的学派是符号主义学派,最早一批人工智能科学家多半是数学家和逻辑学家,他们在计算机诞生后把计算机与自己的研究结合起来,从而进入人工智能领域。在中国,同样是由数学家翻开了人工智能研究的第一页。在1979年,无论是机器证明中的“吴方法”走向世界,还是堪比达特茅斯会议的计算机科学暑期讨论会的举办,其背后都有着数学家的身影。也正是从这一年起,中国人工智能迈开了追赶世界的脚步。
“吴方法”的提出者,正是数学家吴文俊。他与王湘浩、曾宪昌并称“机器证明三杰”。1970年代后期,近花甲之年的吴文俊从研究中国古代数学出发,开创了崭新的数学机械化领域,提出了用计算机证明几何定理的“吴方法”,被认为是自动推理领域的先驱性工作。
1979年1月,应普林斯顿高等研究院的邀请,数学家吴文俊怀揣2.5万美元,登上了赴美交流的班机。与他同行的是数学家陈景润。
二人是中美正式建交后第一批应邀赴美学习访问的科学家,将在普林斯顿高等研究院学习和交流一段时间。陈景润交流的主题自然是“1+2”,而吴文俊此行交流的主要内容,除了他的老本行拓扑学,更多的是中国古代数学史和数学机械化,他想用自己携带的2.5万美元购买一台计算机,用于数学机械化的研究。
吴文俊在1979年获得中国科学院(下称“中科院”)自然科学一等奖时,数学机械化已经成为他的主要研究方向。这个研究方向也受到世人瞩目,吴文俊的研究方法在机器定理证明界被称为“吴方法”,中国智能科学技术最高奖“吴文俊人工智能科学技术奖”就使用了吴文俊的名字,以纪念吴文俊作为中国研究者在人工智能相关领域取得的成就。
1977年春节,吴文俊首次用手算成功验证了几何定理机器证明的方法,后来,吴文俊又在一台由北京无线电一厂生产的长城203上证明了西姆森定理。吴文俊将相关的研究文章《初等几何判定问题与机械化证明》发表在1977年的《中国科学》上,并将文章寄给了王浩。王浩高度评价了吴文俊的工作,并复信建议吴文俊利用已有的代数包,考虑用计算机实现吴方法。
1981年,周咸青到得克萨斯大学奥斯汀分校留学,当时得克萨斯大学奥斯汀分校堪称定理证明界的王者,该校的两个研究小组都曾获得定理证明的最高奖赫布兰德奖。周咸青向罗伯特·博耶(Robert Boyer)提及了吴文俊的工作,博耶觉得很新鲜,便继续追问,但周咸青只知道是将几何转化为代数,具体细节则讲不出所以然。
之后,伍迪·布莱索(Woody Bledsoe)便让周咸青和另一位学生王铁城去搜集资料,周咸青的博士论文便是吴方法的实现。吴文俊很快寄来了两篇文章,文章上都有他给布莱索的签名。在此后两年,这两篇文章被得克萨斯大学奥斯汀分校复印了近百次寄往世界各地,吴方法开始广为人知。