威廉·马库恩。

机器定理证明是人工智能中最古老也最困难的研究领域。在这一领域，威廉·马库恩（1953—2011）可以称得上是最杰出的实干家，他创立的一阶定理证明器Otter是上世纪90年代基于逻辑的定理证明器的集大成者影响了当时整个定理证明领域的理论和实践。

说起机器定理证明，需要溯源到著名的阿贡实验室。

美国阿贡国家实验室。

阿贡实验室的发展脉络大致是这样的：物理学家费米在曼哈顿计划的早期负责核反应堆。战后，美国以费米实验室为基础建立了第一个国家实验室阿贡，隶属于能源部。阿贡实验室的一个分部是应用数学和科学计算。天才的盲人数学家拉里·沃思在这一分部内成立了阿贡机器定理证明小组，为早期的理论发展作出了原创贡献。1984年，沃思把刚从西北大学博士毕业的马库恩招到阿贡实验室，马库恩遂成为20世纪90年代定理证明领域快速发展的重要推动者。

在加入阿贡实验室后，沃思用C语言写了一阶逻辑定理证明器Otter，实现了当时定理证明里最先进的技术。美国人工智能的主要语言一直是LISP，而马库恩为了追随沃斯，也曾和人开玩笑说，自己只会写C语言。

马库恩也是最早把项索引引入机器定理证明器的人。机器定理证明中最花时间的操作是包含测试，即检测一个新生成的定理是不是以前被证明出来过，或者新证明出来的定理是不是包含以前证明出来的定理。如果不做包含测试，机器定理证明器很快就会把内存耗光。很多证明器要花超过95%的时间做包含测试。Otter主要用到了两种项索引，一种是路径索引，另一种是马库恩自己发明的差别树索引。差别树索引对正向包含测试极为有用，极大地提高了证明的效率。

马库恩还利用Otter作为组件开发了另一款专门证明方程的证明器EQP。1996年10月10日，马库恩用EQP证明了罗宾斯猜想——数学家罗宾斯1933年提出的一个猜想，60多年来从未被证明。EQP在一台486机上跑了13天，给出了证明，之后又在一台IBM RS/6000工作站上跑了7天，进行了验证。

解决罗宾斯猜想，被认为是机器全自动证明的第一个尚未被人解决的重要猜想。《纽约时报》报道了这一里程碑事件，马库恩也在第一时间打电话给已经81岁的罗宾斯。

罗宾斯猜想的解决，为马库恩带来多项荣誉，2000年，他获得机器定理证明领域的最高奖埃尔布朗奖。

这里有必要说一下埃尔布朗——一位法国的天才数学家的故事。埃尔布朗生于1908年，他的博士论文为数理逻辑的证明论和递归论奠定了基础。当哥德尔不完全定理刚出来时，他检查了自己的论文，写了一句话作为附言：哥德尔的结果和我的结果并不矛盾。他给比他年长两岁的哥德尔写信讨论递归函数，1931年7月25日哥德尔给他回了信，两天后，埃尔布朗爬阿尔卑斯山时不幸遇险身亡，年仅23岁。为了纪念他，后来定理证明领域的最高奖项以他的名字命名。在埃尔布朗奖不长的名单中，沃思是当之无愧的首届（1992年）得奖人，马库恩是第七届（2000年）得奖人。

机器定理证明领域，面临着瞬息万变的技术变革，也被时代发展塑造着自身命运。2006年，阿贡实验室的定理证明小组被裁掉了，这大概算是符号派低潮的标志性事件。对定理证明作出巨大贡献的马库恩失业了，他那时还不到53岁。

一个时代结束了，另一个时代开启。一年后，马库恩去新墨西哥大学，担任没有终身教职的研究教授。他离开阿贡后，无法对Otter做大的改进，虽然他又有了新证明器的构想，但没时间得到完美的实现，马库恩主导的证明器的性能遂被其他团队逐渐超越。目前最领先的一阶逻辑定理证明器是曼彻斯特大学的“吸血鬼”。

2011年，马库恩因急症去世。他在阿贡的前老板沃思深情地写了纪念文章。毕竟，他们共同开创了一个时代。

有些领域，一开始就把80%的容易问题解决了，而后就一直很难，进展很慢，少有突破。人工智能就是这样，定理证明尤其如此。即使硬件再发达，如果算法和方法论不突破，也很难实现新的进步。也许成功的曙光就在不远的前方，可惜马库恩已经看不到了。

（作者单位：乌镇智库）