送交者: 自如 于 2006-5-26, 12:14:55:
回答: ZT: 凄美的梦：董德周和数学难题“四色猜想” 由 Nixrreg 于 2006-5-26, 10:03:24:
1976年Appel和Haken就已经得到了第一个证明，但他们的归纳分类有上千个，是用计算机验证的，算是Automated Reasoning早期的一个大成果之一。但人们还是不免担心程序有BUG或是程序未必按照正确的算法处理之类。1994年图论的几个大头Robertson,Seymour等等得出了一个简单得多的证明，分类只有数十个，用手都可以验算。图论界以前有一个笑话，外行来听讲座，经常会问：四色猜想真的被证明了吗？这个新证明彻底消除了这个疑问。