|
证明是由美国伊利诺斯州立大学执教的的阿佩尔（K．Appel）与哈肯（W．Haken）两位数学家利用了三台高速的电子计算机，对“四色猜想”进行证明。他们运用了一种“不可避免性”理论，对一万个图进行检验，从中挑出了近两千张特别的图，对每一张地图都使用了二十万种可能的方法着色，计算机作了两百亿个逻辑判定，经过1200小时的计算，终于在1976年6月证明了这个数学名题。由这些图就能证明“地图四色问题”是对的。如果这一过程要人工计算的话，大概得用几十万年的时间。真不可想象！伊利诺斯数学杂志的审稿人，对阿佩尔与哈肯证明的审查，也是通过计算机来实现的。 同一年10月21日英国科学杂志“新科学人”（New Scientist）登了一篇阿佩尔（K． Appel）亲自写解决这个问题的经过的文章。那一期的杂志封面全版登了用红、黄、蓝 、绿涂彩顶点的图。 阿佩尔在那篇文章大约叙述“地图四色问题”的历史，并提到差不多一百年前肯泊的 证明关键想法是正确的：就是找出一个包含特别图的集合。这些特别图具有这样的性 质：任何平面图一定会包含其中一个特别图为子图，而且如果这个图是需要用五种颜 色来涂，那么顶点更少的图也是需用五种颜色来涂的。 20世纪以来，许多人一直在继续按照他的思路，推进着四色问题的证明工作，并且取得了不少成就。可惜这些成就所提供的检验方法太复杂，人们难以实现。 50年来美国、英国、德国及法国数学家找到一些特别图。可是随着顶点数增加，要判断一个图是否特别图就很不容易。自从高速电子计算机出现后，德国数学家亨利·希斯（H．Heesch）就设计一些程序，然后藉助电子计算机来找及验证特别图。 高速数字计算机的发明，促使更多数学家对“四色问题”的研究。从1936年就开始研究四色猜想的海克，公开宣称四色猜想可用寻找可约图形的不可避免组来证明。他的学生丢雷写了一个计算程序，海克不仅能用这程序产生的数据来证明构形可约，而且描绘可约构形的方法是从改造地图成为数学上称为“对偶”形着手。 1960年美国数学家哈肯也开始这方面的工作，1972年阿佩尔和哈肯合作一起改进电子计算机程序，到了1974年工作是有一些眉目，这时参加他们工作还有一些人。在1976年1 月他们找到一个很好的程序，能构造出特别图，并且能很快就验证，这时他们是有信心能解决“四色问题”了。 例如有人在1970年设计的方案，用当时的计算机来算，也需要连续不断地工作十万个小时，也就是说，要连续不断地计算11年以上，才能得出结论，所以难以证实。1970年以后，人们千方百计地改进了证明四色猜想的方案。而且计算机的性能与使用方法也有了很大的变化，为机器证明四色猜想创造了条件。 “四色定理”本身没有什么突出的理论价值和实用价值，人们可以用四种颜色绘制地图，也可用更多的颜色区分填充。但它曲折的证明历程使人深思，激发人们敢于面对困难，迎接挑战，去探索问题的真谛。数学家阿佩尔与哈肯的工作，主要是用电子计算机解决了124年未解决的纯理论问题，成为四色定理。人与机器的合作完全有可能解决那些悬而未决的问题，我们期待着那一日的到来。计算机在证明数学难题方面立下了功勋。这一成果轰动世界，引起了极大的反响。这是一百多年来吸引许多数学家与数学爱好者的大事， 四色猜想的计算机证明，轰动了世界。它不仅解决了一个历时100多年的难题，而且有可能成为数学史上一系列新思维的起点。这是一百多年来吸引许多数学家与数学爱好者的大事，当两位数学家将他们的研究成果发表的时候，当地的邮局在当天发出的所有邮件上都加盖了“四色足够”的特制邮戳，以庆祝这一难题获得解决。 美国数学家的贡献主要不在于证明四色定理本身，而在于用计算机解决了人们多年来无法解决的理论问题。它表明，靠人与机器合作，有可能完成连最著名的数学家至今也束手无策的工作，标志着人类认识能力的一个飞跃，极大地推动了以计算机为基础的人工智能的发展。目前，尚有一些问题留待人们去解决：已有的证明能不能简化？可不可以不用计算机而给出证明？这些问题仍吸引着有志者继续进行探索。 “四色问题”的证明仅解决了一个历时100多年的难题，而且成为数学史上一系列新思维的起点。在“四色问题”的研究过程中，不少新的数学理论随之产生，也发展了很多数学计算技巧。如将地图的着色问题化为图论问题，丰富了图论的内容。 不过也有不少数学家并不满足于计算机取得的成就，直到现在，仍由不少数学家还在寻找一种更简洁的书面证明方法。 钱学森在一篇文章中谈到这件事的意义：“去年数学界哄动一时的一件事，是用电子计算机证明了数学上的四色定理。画地图要求相邻两国不用同一色，一幅地图只需要四种颜色。要证明这个定理很难 ，数学家经过上百年的努力，证明不了。去年美国数学家用电子计算机证明了。他们看到这个问题要证明并不是不可能，而是证明的步骤、程序很复杂，人一辈子的时间也证不完。他们把程序编好，交给高速的电子计算机去干。高速电子计算机也用了一千多个小时才证出来。美国数学家认为，他们的主要贡献不是在证明了四色定理，而在运用电子计算机完成了这件人没有能够完成的事。” |
|
|
