用电脑证明数学定理：人工智能与计算机教学研究

2023-11-15 理论教育版权反馈

【摘要】：1976年6月，伊利诺斯州立大学的两位数学家哈肯和阿佩尔宣布，他们证明了“四色是足够的”，从而使这道长期悬而未决的难题变成了一条真正的数学定理。到了1963年，改进的程序就在大型计算机上证明了罗素—怀特海《数学原理》第二章中的全部52个定理。自动定理证明是人工智能研究领域中一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证明的方法。

在1976年以后，从美国伊利诺伊州厄班纳寄出的邮件，除了盖有通常的邮戳外，还加盖了一个特殊的邮戳，那是一句颇带炫耀口吻的话——“四色是足够的”。

厄班纳人如此炫耀是可以理解的，因为那个特殊的邮戳所纪念的的确是数学史上的一个重大的事件——让数学家们困惑了100多年的“四色定理”，终于由厄班纳的两位居民证明了。

“四色问题”是1952年由一位21岁的大学生最先提出的，他猜想，任何地图都可以只用4种颜色着色，使得任何两个相邻的区域都看上是不同的颜色。

这个问题看上去是那么简单，就是一个小学生也不难理解，结论的正确性看上去也是无可置疑的，谁要是不相信，请他随便画一幅地图试一试好了。但是数学的严谨性要求，任何一个数学命题只有获得了严格的证明，才能被承认为数学定理，而正是这样一个基本的要求，却难倒了100多年来许多优秀的数学家，使四色问题也像“哥德巴赫猜想”这一貌似简单的问题一样，成了一道著名的数学难题。

1976年6月，伊利诺斯州立大学的两位数学家哈肯和阿佩尔宣布，他们证明了“四色是足够的”，从而使这道长期悬而未决的难题变成了一条真正的数学定理。在数学史上，一道难题获得解决的意义往往不在于又增加了一条新的定理，而在于在解题过程中，数学家们发展了数学思想，创造了新的数学方法。

最令全世界瞩目的是，他俩对四色定力的证明是在计算机上完成的。

人们一向把证明数学定理看作是对人的智力的严格考验，现在数学家们还没有解决的问题却在计算机上解决了，难道计算机比数学家的智商还要高一些吗？

对于这个问题不能简单地用“是”或“不是”来回答，让我们还是先看看电子计算机是怎么样完成四色定理的证明的吧。

哈肯和阿佩尔在1972年就开始研究四色问题。他们注意到，英国数学家肯普曾经在1879年发表了一个巧妙的“证明”，基本思路是考虑地图上相邻区域数目不同时的各种可能情况，证明每一种情况下，都不必要使用5种颜色着色。这实际上是使用穷举归纳法，后来人们发现肯普的“证明”中出了错。原因在于，按照肯普穷举归纳法的思路，必须把情况分得足够细，并逐一判断每种情况是否可以“归约”（即是否不必要用5种颜色着色），而这工作的复杂程度，是运用已有的数学技巧由人力所不能完成的。于是，哈肯和阿佩尔考虑让计算机来完成这项工作。他们一方面从理论上继续简化问题，一方面用计算机试算。到了1976年1月，他们认为可以用计算机操作了，于是将他们组出的一种很复杂的程序输入IBM360计算机，让计算机去寻找各种可能的情况（称为“构型”），并逐一判断它们是否可以归纳。(www.chuimin.cn)

事实表明，这项工作对于计算机来说也并不轻松，计算机工作了1200多小时，进行了上百亿次逻辑判断，对1482种构型逐一验证了它们都是可以归纳的，这才修补了100年前“肯普证明”中的错误，完成了四色定理的证明。四色定理的机器证明是一项重大的数学成就，其真正的意义在于它以胜过雄辩的事实，有力地回答了电子计算机究竟能够做些什么。它还重新挑起了一个长期争论不休的话题：电脑能够胜过人脑吗？

计算机能够做什么？这个问题实际上早在电子计算机问世以前就已经有了答案。

英国的图灵是一位对电子计算机理论和技术发展都做出过突出贡献的数学家。1936年，他通过把人的计算活动分解成几个基本的机械动作，提出了一种抽象的计算机模型，即所谓的“图灵机”。图灵机的结构很简单，动作也很简单。我们不妨把珠算盘看作图灵机的一种原型。图灵机由一条打上方格的纸带，每一格都可以写一个数码——珠算盘的每一档就相当于纸带上的方格；图灵机有一个读写头，它在纸带上向左或向右一格一格地移动，同时相应地执行操作指令——我们的眼睛和拨算盘的手指就可以起读写头的作用，也是向左或者向右一档一档地扫描和拨珠；图灵机有一个控制装置，他对读写头发操作指令，并根据读写头所扫描的纸带方格中的数据决定下一个操作步骤（在做珠算时，我们的大脑就起着这样的作用）。手指拨算盘的动作很简单，无非是在某一档上拔或者不拨珠，向右或向左移动一档，停止。图灵机的读写头的动作规则是：在纸带的某一格中写或者不写数据，向右或向左移动一格，停止。我们知道，从理论上讲，人能够执行的算法，珠算盘都能够执行。图灵证明了，人或者其他机器能够执行的算法，“图灵机”都能够执行。这样，他对计算机在理论上能够做什么或者不能够做什么提出了精确的回答。

早在1956年，一些计算机专家就提出了逻辑理论机程序；在计算机中先存储一些公理，再给一些推理规则，然后让机器自己去探索解题的方法，从而证明了罗素—怀特海《数学原理》第二章52条定理中的38条定理。到了1963年，改进的程序就在大型计算机上证明了罗素—怀特海《数学原理》第二章中的全部52个定理。

自动定理证明是人工智能研究领域中一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证明的方法。因此，智能系统不仅需要具有根据假设进行演义的能力，还需要一定的判断技巧。我们知道，一位熟练的数学家可以运用他所掌握的专门知识和判断能力精确地推测出哪些已经被证明的定理在当前的证明中是最有用的，并把主问题分解成为几个子问题，以便独立地处理它们。此外，许多非数学领域的课题，如医疗诊断、信息检索、规划制定和难题求解等，都可以转化成为相应的定理证明问题。

现在，数学家们对数学问题在理论上的可计算性已取得了十分丰富而深刻的研究成果。并不是所有的问题都能够找到可以精确确定的算法，因而不是所有的问题都有理论上的可计算性。例如，在数学中有许多“存在性定理”，其中有些定理既指出了某一问题的解是存在的，也指出了寻找这个解的方法，那么这个问题在理论上是可计算的，也有些定理仅仅指出了某一问题的解是存在的，却不能指出寻找这个解的方法，那么从理论上讲，这一问题就不具有可计算性。

从理论上可以精确确定其一个问题的算法是一回事，实际上这种算法是不是可行则是另外一回事，因为这里还有一个计算时间限制的问题。《十万个为什么》中曾经讲了这样一个问题：如果要求在算盘的高位第十档拨上一颗珠子，规定的算法是从最低位的那一档开始，一颗一颗地加，满十则向上一档进一颗珠子，然后又在最低档上一颗一颗地加，满十再向上一档进一颗珠子，如此反复进行，直到有一颗珠子进到第十档上，这种算法显然是可以执行的，但是需要花费多少时间呢？假定每半秒就可以拨一颗珠子，那么要完成这个算法得花费47年的时间，这显然是人力所难以胜任的。电子计算机的运算速度可以高达每秒上亿次，但是毕竟得花费时间。因此，如果一个问题的算法非常复杂，就有可能连计算机也难以胜任。比如，要求计算机打印出26个英文字母的全部排列组合，从理论上讲并不难，一台计算机每秒能够打印1亿个排列，完成这一算法也得花上百亿年。

事实上，计算是人的一种智力活动，人所不能胜任的计算，计算机可以胜任，从这个意义上说，计算机比入脑更“灵光”。但是，如果没有科学家们为它编写好算法程序，它自己可没有办法“动脑筋”，从这个意义上讲，还是人脑比电脑更聪明。

用电脑证明数学定理：人工智能与计算机教学研究

相关推荐