四色定理与计算机
机器或计算机自动证明数学定理的研究工作是人工智能重要的研究领域。
1957年，人工智能的先驱者之一Simon曾预言，计算机将在十年之内证明具有重要意义的数学定理。十年过去了，Simon的预言未能实现。然而，机器或计算机自动证明数学定理研究工作并未就此停止前进的步伐。
许多具有重要意义的数学定理来自于数学猜想，四色定理定理就是其中之一。 1852年，毕业于伦敦大学的弗南西斯在一家科研单位负责地图着色的工作。弗南西斯发现了一种有趣的现象：“似乎，每一幅地图都可以用四种颜色进行着色，使得有共同边界的国家都被着上不同的颜色。”这个现象能不能从数学上加以证明呢？弗南西斯和他在大学读书的弟弟决心试一试。兄弟二人为证明这一问题而使用的稿纸已经堆成了山，可是研究工作没有进展。于是，弗南西斯的弟弟就这一问题请教自己的老师，著名数学家摩尔根。 摩尔根找不到解决这一问题的途径，于是又写信，向自己的好友，著名数学家密尔顿请教。密尔顿也未能找到解决这一问题的途径。
1872年，著名数学家凯利正式向伦敦数学学会提出了这个问题，于是四色猜想便成了世界数学界关注的问题。
一开始，四色问题并为引起人们足够的重视。数学家们低估了它的难度。德国数论专家闵可夫斯基上拓扑课时说，四色问题之所以一直没有获得解决，那仅仅是由于没有第一流的数学家来解决它。他拿起粉笔，竟要当场给学生进行推导，结果没有成功。下一节课闵可夫斯基继续尝试，还是没有成功。几个星期过去了，闵可夫斯基仍无进展。有一天，闵可夫斯基刚跨进教室，雷声大作。他马上对学生说：“天责我自大，我也无法解决四色问题。” 一百多年来，四色猜想困扰着数学家们，没有人能证明它，也没有人能推翻它。 无数的数学家投身于四色猜想的证明。许多人声称自己证明了四色猜想。然而，最后都被证明是错误的。
1890年，赫伍德证明了五色定理。然而，四色猜想仍然只能是四色猜想。
四色猜想问题刺激了大量的数学研究，促进了图论和拓扑学等相关学科的发展，并获得了许多的应用。
1976年9月，《美国数学会通报》(v.82 n.3) 宣布四色定理被证明。
四色问题是怎么解决的呢？
1976 年 7 月，美国的 Appel 等人用三台大型计算机，耗时 1200 CPU 时间，进行了100亿逻辑判断，证明了四色定理。
四色猜想成为四色定理。当地的邮局在当天发出的所有邮件上都加盖了“四色足够”的特制邮戳，以庆祝这一难题获得解决。
四色定理被计算机证明了。然而，问题是，计算机证明四色定理实用了人工智能技术吗？回答可能是否定的。四色定理的计算机证明程序是纯粹的基于四色具体问题的问题求解步骤，而非人类通用的逻辑思维或逻辑推理，不能应用于其它哪怕是极为简单的数学定理的证明。
一个智能的数学定理的自动证明机器，应该不仅能证明四色定理，还应该能证明哥德巴赫猜想、费马定理、庞加莱猜想，等等
