数学史上的一个奇迹

自2200年前欧几里德提出数学假设证法以来,人们一直困惑于一个证明正确性的检查。任何一个证明中,一行接一行的逻辑推论必须全部正确。也就是说,在检查任何一个证明的正确与否时,必须对整个证明的每一步骤进行验证。检查工作往往比证明更艰巨。 1879年,阿尔弗雷德·肯佩宣称自己证明了数学悬案四色定理——在任何地图上,仅四种颜色总能使相邻两国保持不同的颜色。11年后,人们查出了他的证明中的一个错误。1976年,电子计算机通过几百万个独立的逻辑步骤再次对四色定理进行了证明。但没有人能对这么长的证明予以验证,人们对依靠计算机来证明这一定理仍不放心。