|||
颜料青黄蓝褐,
慢把地图勾勒。
疆域必分明,
求证百年无策。
攻克,攻克,
人在机前羞涩。
相传,四色问题是一名英国绘图员提出来的,此人叫格思里。1852年,他在绘制英国地图的发现,如果给相邻地区涂上不同颜色,那么只要四种颜色就足够了。100年来,无数优秀的数学家企图证明它都以失败告终,四色猜想的证明过程大大促进了拓补学的进展,1936年数学家希奇证明,只要证明10000多种情形下的地图四色猜想成立即可成为定理,但靠笔来算在当时是不可能的。
1972年起,黑肯与阿佩尔开始对希奇的方法作重要改进。到1976年,他们认为问题已经压缩到可以用计算机证明的地步了。于是从1月份起,他们就在伊利诺伊大学的IBM360机上分1482种情况检查,历时1200个小时,作了100亿个判断,最终证明了四色定理。在当地的信封上盖“Four colorssutfice”(四色足够了)的邮戳,就是他们想到的一种传播这一惊人消息的别致的方法。
人类破天荒第一次运用计算机证明著名数学猜想,应该说是十分轰动的。但说穿了,这种方法其实是“穷举法”,严格来说不能叫“证明”。直到现在为止还没有人能给出严格的逻辑推理证明,所以四色定理的证明,是说人类聪明呢,还是计算机在嘲笑人们愚蠢呢?
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-9-1 17:11
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社