四色定理的三代证明_王献芬

四色定理的三代证明* 王献芬 胡作玄 (河北师范大学数学与信息科学学院,河北石家庄 050016) 摘 要:四色猜想是图论中的一个重要问题。它从猜想到定理历经三代证明: 1976年阿佩尔和哈肯的 计算机辅助证明、1994年西缪尔等人的修正、2005年贡蒂埃的形式证明。每一代证明都有其特点和不足。 本文对这三代证明进行了简单的评述, 说明由一个经验来源的问题如何逐步得到解决并在发展过程中形成 诸多新的数学分支。它的重要性不在于结果本身而是从它的证明中可学到的潜在道理。本文提出数学证 明的一个方面, 即用有限驾驭无穷,同时在四色定理的证明史中表明简化永远是数学方法的灵魂。 关键词:四色定理 计算机辅助证明 形式证明 数学证明 图着色理论 1中图分类号2 N0 1文献标识码2 A 1文章编码21000 - 0763( 2010 ) 04 - 0042 - 07 数学并非一门经验科学, 其中绝大多数问题有着非经验的来源。甚至叙述起来最简单的问题或定理, 都需要一定的概念(理性)支持,而且很难用经验的方法来证实。典型的问题有三角形内角和为180b,虽然这 些概念都很直观,但是,对无穷多三角形无法一一用经验方法证明, 甚至发现这个问题也需要理性的思考, 而一般人根本想都想不到。另一个问题就是熟知的哥德巴赫( C. Goldbach, 1690- 1764)猜想。虽然哥德巴 赫在试验的方法下通过验证提出猜想, 但它首先必须先有素数的概念。虽然人们穷其一生可对有限的情形 进行验证, 但这并非证明,因为验证只能对有限的情形说对或不对, 而不能对无穷多情形说对。因此数学的 证明本质上是非经验的(除非通过经验的办法提出反例) , 而且正面的证明是/用有限驾驭无穷0。康托尔 (G. Cantor, 1845- 1918)说,在数学的领域中, 设问的艺术有时要比解题的艺术更重要。爱因斯坦也说过类 似的话。物理学的问题大都有经验的来源,例如,怎样做交换超导体? 它的前提首先是实验室中已发现超 导现象。数学的问题则大不相同,绝大多数问题是内生的。许多人都认为追根溯源数学概念是从经验中归 纳得出的, 但是,数学发展到今天,已经脱离开实际很远了。对于非本专业的人来说, 理解一个简单的数学 问题都是十分困难的,例如庞加莱猜想: 3维单连通闭流形一定是 3维球面。就牵涉到维数、单连通、闭、流 形、3维球面等五个概念,而且 3维球面根本在现实世界中也是摸不着、看不见的东西, 无从谈到经验, 只能 靠数学家的想象以及由此产生出的抽象的、严密的理论。 当然, 在现实生活中,人们从实践中也的确提出过一些经验问题。四色问题就是其中最为典型的一个。 这种问题在数学问题的汪洋大海中往往显不出它的重要性, 因此常常被边缘化。由于这种问题提法简单明 确,通常被许多数学爱好者以及一些数学家看成是对数学智力的挑战。当有修养的数学家也遇到困难时, 往往会有一些大数学家认真对待这类问题,甚至由此导致问题的解决。 这种经验来源的问题虽然本身并非主流, 一旦被大数学家重视, 经过他们的研究、发展及推广, 往往会 形成繁茂的数学分支,进入数学的主流当中。 本文就试图通过四色问题的解决过程来阐明一个经验来源的数学问题如何解决, 如何发展壮大形成图 论的核心分支。 * 本文为国家自然科学基金资助项目(项目编号: 10971049)和教育部博士点专项基金的研究成果之一。 1收稿日期22009年 12 月 21日 1作者简介2王献芬( 1981- )女,河北邯郸人, 河北师范大学数学与信息科学学院博士, 主要研究方向为代数图论、拟阵论及近 现代数学史。 胡作玄( 1936- )男,北京市人, 中国科学院数学与系统科学研究院研究员, 河北师范大学数学与信息科学学院教 授,研究方向为近现代数学史。 42 一、问题的提出与解决概述 四色问题来源于绘制地图的实践。当绘制一幅地图时, 往往需要用不同颜色将相邻区域区别开来, 这 样四种颜色是否就够了呢? 这里的相邻区域是指具有公共边界的区域。当两个区域仅在有限的点处邻接 时, 用同一种颜色即可。1852年, 葛斯瑞( Francis Guthrie, 1831- 1899)在给一张英国地图染色时猜想: 对任 意地图染色,四色足够。112,122他曾写信问弟弟弗雷德里克( Frederick Guthrie)能不能给出数学证明。弗雷德 里克无法解答,便拿去请教著名数学家德#摩根( A. De Morgan, 1806- 1871)。德#摩根虽证明了地图上不存 在五个国家彼此都相邻的事实,但是地图所需色数不等于相邻国家数的最大值。证明四色问题需要更有 力的数学方法。 同年 10月 23日,德#摩根致信当时最伟大的数学家、物理学家哈密顿(W. R. Hamilton, 1805- 1865) , 然 而得到的答复却是对染色问题/不感兴趣0。之后,为引起其他数学家的关注,德#摩根继续用各种方式传 播四色问题。目前所发现的第一个正式的文字记录,是他在 1860年 4月 14日发表的一篇书评( 112, p. 92)。 除德摩根外, 英国大数学家凯莱( A. Cayley, 1821- 1895)对四色问题的早期传播也做出了巨大贡献。 1878年 6月 13日,他在伦敦数学会上当场发问是否有人证明了四色问题。次年,他还在5英国皇家地理学 会会报6发表论文, 第一次从数学的角度明确陈述了这一猜想,并指出了证明的困难所在,最后他表示/ 还 不能给出证明0132。大数学家对四色问题的关注自然也激发了其他人的求解欲望。在那个时候, 一种普遍 的观点却是四色问题应该不会太难,或许很快就能解决。然而, 事实证明并非如此。 四色问题从猜想到定理历经三代证明: 1976年阿佩尔( K. Appel, 1932- )和哈肯( W. Haken, 1928- )的 计算机辅助证明, 不过这个证明在长达 20年内未能获得一致认同, 原因在于证明中使用了计算机, 且无法 用手算核实;而理应用手算核实的部分又极其繁琐以至于没有人能够独立进行验证。鉴于此, 1994年, 西 缪尔( P. Seymour, 1950- )、罗伯逊( N. Robertson, 1938- )、桑德斯( D. P. Sanders)和托马斯( R. Thomas)做出 了属于他们自己的证明。二代证明虽然也使用了计算机,但它达到了单独人工复核的 标准 excel标准偏差excel标准偏差函数exl标准差函数国标检验抽样标准表免费下载红头文件格式标准下载 ,且在几分钟内 就能用计算机辅助验证, 从而消除了人们对一代证明有效性的怀疑,有力地肯定了四色定理的正确性。尽 管如此,隐藏在计算机内部的逻辑步骤终究不够透明。2005年,贡蒂埃( Georges Gonthier)的形式证明就是 一种把所有逻辑步骤都写出了的证明, 这第三代证明不仅强烈肯定四色定理确是一个定理,而且对数学和 计算机科学都有着十分重要的意义。 每一代证明都不是在平地上创造出业绩的, 许多先驱者的工作为他们铺平了道路。第三代证明基本 上是对第二代证明的逻辑步骤的机器检验和确认;第二代证明是对第一代证明的修正; 第一代证明则是建 立在肯普( A. B. Kempe, 1849- 1922)的思想方法基础上的。下面分别概述四色定理的这三代证明及其思 想传承关系。 二、一代证明( 1976年) 在四色定理的一代证明中, 从逻辑上讲,第一步是用放电法构造不可避免集; 第二步是证明不可避免 集中每一个构形的可约性。然而在历史上,首先得到的是许多可约性论据。肯普以后, 美国数学家伯克霍 夫( G. D. Birkhoff, 1884- 1944)首先取得了可约性理论的一些进展。142其后,德国数学家希什 (H . Heesch, 1906- 1995)提出了放电法, 最终由阿佩尔和哈肯借助计算机证明了四色定理。下面简要概述为一代证明 直接做出贡献的数学家们的工作。 11一代证明的经过 1879年, 肯普宣称/证明0了四色定理152。但 11年后被发现有缺陷。这立即引起许多大数学家的注 意, 其中包括伯克霍夫、麦克莱恩( S. Mac Lane, 1909- 2005)、惠特尼( H. Whitney, 1907- 1989)等大数学家。 事实上, /几乎每一位大数学家都曾在某个时候试图解决四色猜想,且都曾暂时认为自己成功了0162。然 而, 与肯普一样,他们的论证同样经不起时间的考验。不过,肯普的/ 证明0却为后世数学家提供了解决问 43 题的突破口,其中蕴含了解决四色问题的必不可少的思想和方法。 四色问题的难点之一是涉及无穷: 研究对象是无穷多个任意地图。利用欧拉公式, 肯普证明任意地图 都伴随有一个至少需要同样多颜色的正规地图, 于是,问题就变成对正规地图证明四色足够。尽管如此, 还是无法避免无穷多的困扰。对此,肯普使用了归谬法: 先假设存在需 5种颜色才能染色的正规地图, 然 后寻找矛盾,从而证明四色足够。 在寻找矛盾的论证过程中, 肯普隐约地引入了两个概念:不可避免性和可约性。第一个概念源于正规 地图的性质。任意正规地图至少有一国具有 2、3、4或 5个邻国,换言之, 2个、3个、4个和 5个邻国的/ 构 形0是不可避免的。所谓可约性,是指从正规地图中移去某个子图, 所得新图的可四色性蕴含原图的可四 色性。这样的正规地图就称为可约的; 而被移去的子图就叫做可约构形。肯普的出色想法是,只要能证明 不可避免集中的每个构形都是可约的, 四色问题就证出来了。 接下来,对于事先假定的五色地图,他分成以下四种情况检查构形的可约性: ( i) 2个邻国; ( ii) 3 个邻 国; ( iii) 4个邻国; ( iv) 5个邻国。显然,如果都可约,就与需要 5种颜色产生矛盾,从而证明四色定理成立。 然而,他提出的/肯普链0方法只是正确证明了( i) - ( iii)三种情况, 遇到( iv)时却失败了, 原因是两次使用 肯普链而导致疏漏。这个缺陷由希伍德( P. J. Heawood, 1861- 1955)在 1890年首先指出(希伍德通过修补 肯普的证明得到了著名的五色定理)。172/定理0重新变回/猜想0。从此, 数学家便意识到, 四色问题可能要 比预想的难得多。 19世纪末是四色问题发展的一个分水岭。肯普虽然未能成功,但他的证明路线为后人指明了方向:寻 找可约构形的不可避免集。1913年, 伯克霍夫发现了大量新的可约构形,而且这些构形比肯普所发现的要 大得多。尽管如此,它们仍然不足以形成一个不可避免集。在这种搜集可约构形以形成一个不可避免集 的道路上, 四色问题进展很慢。那个时候, 一些人开始认识到困难仍出在肯普未能证明的( „) , 具体说就 是( „)分得还不够细。 希什首要的技术贡献是他猜测存在一个有限的可约构形的不可避免集。1950年, 他指出,不仅可以找 到这样一组不可避免集,而且其中构形的个数应有一个上限 ) ) ) 约 1万! 也就是要把情况分细到可以证 明的地步, 大约要分 1万种情况才行! 阿佩尔和哈肯在宣布他们的主要结论之前, 就特别指出: /我们的工作受到了希什182,192研究四色问题的启发, 特别是他猜想11969, 11页, 216页2存在 一个可 4色的可约构形的有限集合 S, 使得每一个可平面图至少包含 S 中的一个构形,,1970 年,希什还得到了一个未发表的结论, ,他称之为四色问题的有限化。01102 希什还是继肯普之后第一位公开宣称四色问题能够通过寻找可约构形的不可避免集来证明的数学 家。他在前人工作的基础上大大发展了可约构形理论,提出了构造可约构形不可避免集的更为普遍的方 法, 其主要思想就是确定一个具有下述性质的构形集合 S:首先,每一个平面图必定包含 S中某一构形; 其 次, 假定平面图包含 S中某一构形且其余部分可用至多 4种颜色着色,那么通过调整着色的方式就能扩展 到整个平面图上来。他关于 A- 可约、B- 可约、C- 可约、D- 可约构形的概念是由伯克霍夫等人的工作 发展而来的182。 希什还是第一位使用计算机研究四色问题的数学家192。他知道把证明构形可约性的现有方法形式 化:他观察到其中至少有一种方法(是对肯普所用方法的直接推广)在原则上是计算机所能做的纯机械过 程。 1969年,希什发明了一种放电法,用来寻找构形的不可避免集。如果一个图不可四色, 那么它必定存 在某个局部障碍。放电的目的就是把这些局部障碍列一个清单出来, 而这些局部障碍实际上恰是肯普所 谓的/不可避免的构形0。希什的这项成就为计算机辅助寻找可约构形铺平了道路。此外, 值得一提的是, 希什对哈肯个人也有很大帮助和影响, 他将自己许多未发表的思想都介绍给了哈肯1112。 1972年,阿佩尔开始与哈肯合作。与希什一样,他们也意识到离开计算机的辅助是不行的。但比希什 英明的是, 他们充分考虑了检验可约性所需机时和存储空间问题。这样,他们一方面在希什约化理论的基 础上继续简化问题,另一方面利用计算机的试算以及人机对话获得有益的信息, 其目的是希望进一步缩减 不可避免集中构形的个数,使证明可约性所需时间和空间降到可以接受的程度。 1976年初, 阿佩尔和哈肯找到了一种新的放电程序, 构造了一个含有 1936个构形的不可避免集。为 44 验证这些构形的可约性, 他们一方面修改科赫( J. Koch)的可约性程序,一方面利用伯克霍夫的更一般性的 约减步骤改进程序, 最终在 IBM360计算机上耗费 1200小时验证了构形的可约性。1976年 6月,他们在5美 国数学会通报6上宣布证明了四色定理 ¹ 。第二年, 5伊利诺斯数学杂志6刊出他们的论文/每个平面地图 都可四色01112,1122。全文长达 139页,另附有计算机程序的微缩胶片 400页, 共分两个部分: 第 Ñ部分/ 放 电0,描述了用来构造不可避免集的放电方法, 给出了证明的全部策略; 第 Ò 部分/可约性0, 刻画了计算机 程序的实现过程, 并列出了 1482个可约构形的不可避免集º。 21对证明的置疑 阿佩尔和哈肯的工作意义已经超过了证明一个数学难题本身, 它告诉人们计算机不仅可以用来计算, 还能用于数学的逻辑证明。然而他们的方法本质上是一种穷举检验法,令人满意的答复绝不是由于/检验 了千百万种情况, 且它们都对01132。这种史无前例地使用计算机辅助证明的做法成了争论的焦点! 哲学家提莫志克( A. T. Tymoczko, 1943- 1996)是怀疑论者的一位代表。他认为一个证明至少应具备 以下三个特征: / ( a)有说服力( convincing) ; ( b)可被检查( surveyable) ; ( c)可被形式化( formalizable) 0。1142他认 为阿佩尔和哈肯的证明不满足( b) , 理由是证明细节隐藏在计算机内,没有谁能够对它进行复核。他表示, 如果数学允许使用计算机进行/实验0, 数学将会面临走向经验科学的危险。如果承认阿佩尔和哈肯的证 明有效,那就是强迫大家改变/数学证明0的含义: 将计算机实验视为确定数学结论的一种新方法。有关数 学证明的探讨详见斯瓦特( T. Swart) 1152 ,戴维斯( P. J. Davis)和赫什( R. Hersh)1162以及罗塔( G- G. Rota, 1932- 1999) 1172。 怀疑论者除了抱怨证明不 /可被检查0外, 还指出证明/不够透明0。代表人物有著名数学作家、评论 家斯图尔特( Lan Stewart)以及数学家布朗( G. Spencer- Brown)。1182 雪上加霜的是, 20世纪 80年代初开始传言一代证明中出现了重要错误, 导致这种传言的原因是人们 误解了施密特(U. Schmidt)复核证明时的一个结论。1985年, 日本的佐伯( S. Saeki)也发现过一个构形描 述上的小错误。不过,幸好这些错误并非本质的, 很快就得到了纠正。除此之外,不包括一些打印错误, 没 有再发现任何致命的错误。1989年, 阿佩尔和哈肯专门为四色定理的证明撰写了一部专著 ) ) ) 5每一个可 平面图是可四色的6。书中补充了证明的细节,并修正了已发现的所有错误, 同时附上了所有缩微胶片的 印刷版,整个证明长达 741页1192。这是他们最后一次对四色定理证明的整理。 尽管如此,一代证明的/两大派别0依旧相持不下:一方面是怀疑论者, 他们反对计算机辅助证明; 另一 方面是支持者,他们接受计算机向数学领域提供的巨大帮助。但无论哪一方, 他们的评述都不是指向阿佩 尔和哈肯本身, 而是针对无法复核整个证明而言。简言之, 一代证明无法单独人力完成并进行验证, 因此 还不能算作一个完美的数学证明。 三、二代证明( 1994年) 1976年,阿贝尔和哈肯虽然使用计算机辅助证明了四色定理, 但是他们的证明并未获得普遍认可, 主 要原因有二:一是使用计算机的部分无法用手算核实; 二是应该用手算核实的部分因过于繁琐, 无人能够 独立完成。这些不太令人满意的地方导致人们对定理的真实性持以怀疑态度, 甚至上升到了对数学证明 含义的哲学探讨。可悲的是,时至今日,很多人却以为就只有这么一代证明! 事实上,第一代证明以后,数学家们并没有放弃寻求严格的数学证明, 也因此推动了图论整个学科的 发展,使得这门学科中大多数问题都与染色问题有关。20世纪 80、90年代, 罗伯逊、西缪尔、桑德斯和托马 斯一直致力于研究染色问题,取得了大量惊人的结果。1994年,西缪尔等四人宣布得到了一种更为简化的 证明。他们以阿佩尔和哈肯的证明为基础, 做出了属于他们自己的证明。这代证明不仅证实了阿佩尔和哈 ¹ 当年许多报社和期刊都纷纷报道了这一消息, 分别是The T imes( 7月 23 日) , SIAM News( 8月) , Science( 8月 13 日) , The Toronto Globe( 8 月 24日) , Le Monde( 8 月 1 日) , Time( 9 月 20 日) , The New York Times( 9 月 24、26 日) , Scientific American( 10 月 ) , New Scientist( 10月 21 日)以及 Die Neue Z™rcherZeitung( 10月 24 日)。 º这是从 1936个构形中除去异构体、子构形等多余构形后所得数目。 45 肯的方法能够证明四色定理,而且澄清了长期以来人们对四色定理真实性的种种置疑,肯定了它的正确性。 1. /四色定理的进展0 ) ) ) 国际数学家大会 1小时报告 1994年,西缪尔在瑞士苏黎世召开的国际数学家大会上宣布,他和另外三位数学家对阿佩尔和哈肯的 证明进行了修正。1202 会上, 西缪尔肯定了阿佩尔、哈肯的巨大成就, 同时指出了造成如此大非议的主要原因。为验证定理 的正确性,西缪尔等四位数学家原打算复核证明,但进行了大约一周以后,他们就放弃了。因为这种做法 比给出新证明还要困难。西缪尔说: /我们决定用阿佩尔和哈肯的方法做出我们自己的证明,细节是属于我们自己的创新,这样 做可能更容易,也更有意义。0( 1202, p. 184) 于是就出现了所谓的第二代证明, 这二代证明实际上是对一代证明的修正。 2.一、二代证明的比较 西缪尔等人证明四色定理的基本思想与阿佩尔、哈肯的大致相同。但为了避免陷入阿佩尔和哈肯的 复杂论证, 他们事先证明了希什关于不可避免性的一个猜想1212。进而, 他们尽量/简化了0整个证明过程。 与一代证明相比, 这种简化体现在1222 : ( a)使可约构形的不可避免集尽可能小。 ( b)使放电法则的数目尽可能少。 ( c)使计算机程序的运行时间尽可能短。 ( d)使证明的非计算机部分(即写在纸上的那些)尽可能简单。 但遗憾的是这些目标有的相互冲突。例如,可以把两个或多个法则替换为一个法则,但要以增加不可 避免集中构形的个数为代价。这种矛盾迫使他们必须对( a )和( b)做折中考虑。除此之外, 他们还遇到了 需/付出更高代价0的地方,即选择可约性的证明方法。(1222, pp. 24- 25) 尽管这有点像修正主义,但他们的努力终究没有白费。1995年 5月 25日, 西缪尔等人将修正后的证 明提交给了5组合学杂志6( B辑)。1997年正式发表出来。它成为四色定理的第二代证明。这个证明只有 43页,较长达 741页的第一代证明而言, 二代证明的确简化了不少:放电法则从 486个减至 20个; 不可避免 构形从 1482个减至 633个;图着色算法由4次时间算法优化为2次时间算法;证明所需机时由1200小时缩 短到 24小时;而且第二代证明达到了人工复核的要求;如果用计算机验证, 只需 5分钟就能完成! 更重要 的是,第二代证明已经没有第一代证明的缺点,也就是第二代证明已经完全没有第一代证明中只有计算机 才能完成的验证过程。换言之, 第二代尽管也要用计算机, 但这种证明对人来讲是更透明的, 每一步都可 以转换成人可理解的证明,虽然它还不完全是一个标准的数学证明。时至今日, 四色问题还没有一个通常 意义下的数学证明。 四、三代证明( 2005年) 尽管二代证明肯定了一代证明的有效性, 但这前两代证明中仍然存在一些不尽人如意的地方。2005 年, 也就是西缪尔的二代证明宣布十年之后,英国剑桥研究院的高级研究员贡蒂埃成功给出四色定理的第 三代证明。1232 这第三代证明并非数学证明,而是所谓的形式证明( formal proof)。对于一个定理, 有了形式证明同有 了数学证明一样, 是一条被证明的定理。更确切来讲, 有了形式证明的定理获得了更强的支持, 因为大多 数数学定理只有数学证明而没有形式证明,反过来,一个有形式证明的定理必定是建立在更广意义上的数 学证明(即包括通常意义下的数学证明,也包括计算机协助下的数学证明)基础上的。从这个意义上来讲, 形式证明的提法对数学和计算机科学有着十分重要的意义, 特别是: ( 1)它强烈肯定四色定理的确是一个定理。 ( 2)对于大量的、已有数学证明的数学定理, 如何找出一个形式证明,这给数学家与计算机科学家提供 了一个新的、广阔的研究领域。 46 对于十分繁复的数学证明, 如何设计计算机程序来验证它是否正确? 从数学发展来看,几十页上百页 的证明已经司空见惯。华裔数学家陶哲轩在从组合学、数论到调和分析、偏微分方程到数理统计等七、八 个领域已发表 200多篇论文,每篇都超过 50 页。单群分类的定理几千页; 几何测度论的大定理 1728页。 这就使某些人置疑数学定理乃至大多数数学家的工作。因此,这种程序是极为重要的。 数学发展必然要走向全盘自动化, 特别是其中可机械化的工作。中国数学家吴文俊在这方面开了一 个头。但形式化证明是另一个发展方向。 形式化证明,简单说, 就是完全符号化,把所有逻辑步骤都写出来的证明, 这样, 它比通常证明要长上 几十倍甚至几百倍,而且都是用符号表示出来,通过推理规则来推理。通常的数学证明使用公理化, 概念 都有明确的定义。形式证明不仅包括这些,而且包括符号串,构成规则、推演规则以及逻辑公理, 这些我们 称之为形式化过程。 由于形式化过程十分繁琐, 形式证明只在 50年前才开始崭露头角。形式证明的元年恰巧是四色定理 形式证明前 50年 ) ) ) 1954年。这一年,数学家M.戴维斯( M. Davis)用普林斯顿高等研究院的冯#诺伊曼 ( J. von Neumann, 1903- 1957)主持研制的计算机 ( Johniac)证明一个平凡的数学定理, 偶数加偶数是偶数。 五年之后, 王浩取得突破,证明罗素( B. Russell, 1872- 1970)、怀特海(A. N. Whitehead, 1861- 1947)的名著 5数学原理6中几百条数理逻辑的定理。当然, 数理逻辑的定理易于证明在于它已经充分形式化。1968年 荷兰数学家布吕言( N. G. de Bruijn, 1918- )设计了第一个验证数学证明正确性的计算机程序,并用来验证 一些数论的命题。其后通过形式化,证明一些简单的数学定理, 如微积分基本定理、代数基本定理、二次互 反律等。这里我们还应该提到 1986年形式证明数理逻辑的大定理 ) ) ) 哥德尔( K. GÊdel, 1906- 1978)第一 不完全性定理。 对于数学定理形式证明的真正突破是 2004年贡蒂埃形式证明四色定理。他的思路分成两部分: 首先 是写下西缪尔的证明的形式部分,其次还要写下另一个不同的程序来验证上述证明是正确的。主要困难 在于,即使语言足够丰富,也很难产生出形式证明。这正好是第三代证明的创新所在。 为了克服这个困难, 数学家不仅仅注意局部的明显性与正确性,而且还必须对整体证明的结构有足够 清楚认识, 而这正是数学家的眼光。他必须能够发现结构的对称性、能够简化、能够推广,而这是计算机做 不到的。因此,通过数学证明的定理很多仍然没有形式证明,这也正是形式证明必须要有数学家的创新之 处。从某种意义上来讲, 这不仅仅是一个形式化过程, 更是一个新的程序设计, 同时还要有自己的或新的 验证程序来验证它正确。这样形式证明才得以完成。 第三代证明的有效性是由不同程序进行复核的客观数学事实, 而程序本身的正确性可以通过运行多 种输入程序凭实验确定。贡蒂埃认为他的成功可以确认:程序方法用于定理证明可能比传统的数学方法 更有效,至少对那些有计算机知识背景的人尤其如此。他说1242,1252 : /与大多数合乎传统习惯的经典数学结论的发展一样, 我们的工作最有意义的方面也并不在 于得到哪些结果, 而是在于这些结果是如何得到的。我们认为我们的成功在很大程度上是由于 把四色定理主要看作是一个程序设计问题,而不是一个形式化问题。我们不是在试图重复一个 精确的、近乎- 形式的数学文本,尽管我们确实大量使用了罗伯逊等人的工作,尤其是他们的组 合分析,但是这里大部分证明主要还是我们自己的。0 2005年 3月, 贡蒂埃给出这样一个形式证明:依据西缪尔等人的证明,设计一个新的证明程序;用 Coq 这个证明辅助器完全验证该程序正确。但我们不能说数学家对这种新事物 评价 LEC评价法下载LEC评价法下载评价量规免费下载学院评价表文档下载学院评价表文档下载 很高, 西缪尔在 2008年 1 月 17日谈到: /它基本上是我们的证明的机器确证。0( 1242, p. 203)对于数学家来讲, 更为令人信服的方法 当然是纯粹数学的证明, 越简单越好。 五、结 语 虽然有很多置疑,四色问题究竟已经成为定理。对于数学问题,数学家感兴趣的主要是技术及方法方 面的问题, 这是他们的专业。但是, 从知识创新的高度来看, 数学家更要关注问题的来源,数学方法特别是 47 数学证明的实质, 以及数学问题在解决过程中所带来的后果。像四色问题这类问题尽管中学生也能明白, 但除此之外,对数学证明的理解也是十分重要的。本文提出数学证明的一个方面, 即用有限驾驭无穷, 同 时还在四色问题的证明史中表明简化永远是数学方法的灵魂。即使有了计算机, 它所能执行的机械化步 骤也是有限的,不简化我们也许需要宇宙年龄数量级的机时。 数学的问题成千上万,数学家不愁无事可做。可是重要的数学问题一定是能大批繁衍后代的问题, 它 们不仅能产生新的概念、新的方法, 而且能创造新的学科、新的问题。四色问题正是这样的问题。它推动图 论的发展,成为图论的核心部分, 激起了许多重要的新的数学思想的形成,产生出大量理论及应用的分支。 例如图的着色理论,已经发展成为一个深刻、漂亮的研究领域1262。把地图四色问题推广到任意曲面上推动了 拓扑图论的发展。例如,一个平面或球面上的地图,四色是足够的,那么在环面(轮胎面)上,四色就不够了,至 少需要七色才行。另外,对图的平面性的研究在缩图理论中达到了高潮。图论在网络理论中的作用更是不 言而喻,在当今的网络世界中离开图论可以说是寸步难行。抚今追昔,这一切均由四色问题所赐。 1参 考 文 献2 112Norman L. Biggs, Lloyd E. Keith, R J. Wilson. Graph Theory 1736- 1936 1M2. Oxford: Clarendon Press, 1986: 134. 122K. May. The Origin of the Four- Color Conjecture1J2. I sis. 1965, 56, pp. 346- 348. 132A. Cayley. On the Colouring of Maps1J2. Proceedings of the Royal Geographical Society ( New Series) . 1879( 1) : 259- 261. 142G D. Birkhoff. The Riducibility of Maps1J2. Amer . J. Math. 1913, 35, pp. 115- 128. 152A B. Kempe. On the Geographical Problem of the Four Colours1J2. American Journal Mathematics . 1879( 2) : 193- 200. 162H. Whitney, W T. Tutte. Kempe Chains and the Four Color Problem1J2. Utilitas Mathematica. 1972( 2) : 241- 281. 172P J. Heawood. Map- Colour Theorem1J2. Quart. J. Pure. Appl. Math. 1890, 24: 332- 338. 182H. Heesch. Untersuchungen Zum Vierf arbenproblem 1M2. Mannhiem, 1969. 192H. Heesch. Chromatic Reduction of the Triangulations, T e , e = e 5+ e71J2. J . Combin. Theory ( Ser B) . 1972, 13: 46- 55. 1102K. Appel, W. Haken. The Existence of Unavoidable Sets of Geographically Good Configurations1J2. Illinois J . Math. 1976, 20: 218 - 297. 1112K. Appel, W. Haken. Every PlanarMap is Four Colorable, Part Ñ : Discharging1J2. Illinois Journal of Mathematics . 1977, 21: 429- 490. 1122K. Appel, W. Haken. Every Planar Map is Four Colorable, Part Ò : Reducibility1J2. Illinois Journal of Mathematics . 1977, 21: 491- 567. 1132T. Gowers, J L I. Barrow- Green, The Princton Companion to Mathematics 1M2. Princeton and Oxford: Princeton University Press. 2008: 696- 698. 1142T. Tmoczko. The Four- Color Problem and Its Philosophical Significance1J2. The Journal of Philosophy . 1979, 76( 2) : 57- 83. 1152E. R. Swart. The Philosophical Implications of the Four- Color Theorem1J2. American Math. Monthly . 1980, 87: 697- 707. 1162P. J. Davis, R. Hersh. The Mathematical Exp erience 1M2. Boston: Birhauser, 1981: 380- 390. 1172G. C. Rota, The Concept of Mathematical Truth1J2. The Mathematical Scientist. 1990, 15: 65- 73. 1182R. Wilson. Four Colors Suffice: How TheMap Problem was Solved 1M2. Princeton and Oxford: Princeton Universtiy Press. 2002: 164- 168. 1192K. Appel, W. Haken. Every Planar Map is Four Colorable 1M2. Providence RI: American Mathematical Society. 1989. 1202P. Seymour, Progress on the Four- Colour- Theorem1C2. Zurich, Switzerland: Birkhauser Verlag, Basel, Switzerland. 1994. 1212R. Thomas. An Update on the Four- Color Theorem1J2. Notices Amer . Math. Soc. 1998, 45( 7) : 848- 859. 1222N. Robertson, D. Sanders, P. Seymour, R. Thomas. The Four- Color Theorem1J2. Journal of Combinatorial Theory ( Ser. B) . 1997, 70: 2- 44. 1232G. Gonthier. Formal Proof: The Four- Color Theorem1J2. Notices of the AMS. 2008, 55( 11) : 1382- 1393. 1242A. Soifer . The Mathematical Coloring Book 1M2. Springer, 2009: 195- 205. 1252G. Gonthier. A Computer- Checked Proof of the Four Colour Theorem. http:PPresearch. microsoft. comPen- usPumPpeoplePgonthierP4co- lproof. pdf. 1262Tommy R. Jensen, B. Toft. Graph Coloring Problems 1M2. New York: Wiley, 1995: 2. 1责任编辑 王大明2 48 The Debate on the Intension and Remission of Qualities in the Medieval Natural Philosophy( p. 35) ZHANG Bu-tian ( Institute for the History of Natural Science, CAS, Beijing ) Abstract: The problem of intension or remission of qualities has resulted in great debates in the medieval natural philosophy. It can be formulated in two ways: ( 1) the ontolog ical question, i. e. , what is the thing that changes in the alteration? There are two main solutions. One is that the quality doesn. t change and the subject participates in the quality in different degrees. The other is that the quality as such changes. ( 2) the physical question, i. e. , how does the intension or remission of qualities happen? There are also two main solutions, that is, the addit- ion theory and the succession theory. Making clear the details of this debate helps us to better understand the problem of motion. s continuity and the mathematization of nature in the early modern age. Key Words: Intension of qualities; Remission of qualities; Addition theory; Succession theory Three Proofs of the Four-Color Theorem( p. 42) WANG Xian- fen, HU Zuo-xuan ( College of Mathematics and Information Science, Hebei Normal University, Shijiazhuang, Hebei) Abstract: The four- color conjecture is one of the most important problems in graph theory. It has been changed into the four- color theo- rem through three proofs: computer- assisted proof by Appel and Haken in 1976, the update version on the four- color theorem by Seymour et al in 1994 and the formal proof by Gonthier in 2005. But there are characteristics and deficiencies in each one. The present paper reviews the three proofs and shows that how the empirical problem was solved gradually and how it got many branches of mathematics formed in the process of its development. But its significance lies not in the results itself but in the potential arguments learned from its proofs. This paper puts one aspect of mathematical proof, namely, to dominate infinite through finite. The history of the proof of the four- color theorem also illustrates that simplification is always the spirit of mathematical method. Key Words: The four- color theorem; Computer- assisted proof; The formal proof; Mathematical proof; Graph coloring theory Kuhn. s / Sources for History of Quantum Physics0 ( p. 49) HOU Yu-de ( Department of Physics, Taizhou University, Linhai, Zhejiang) Abstract: Quantum physics, especially, quantum mechanics, is one of sciencebranches which has the largest effect and change on hu- man society . Thomas Kuhn was one of the most outstanding scientific philosopher in the 20th century. With the help of the specialists in phys- ics, in the history of science and in the philosophy of science, he finished the project which was named / Sources for History of Quantum Phys- ics0 . The sources are very important and are worth understanding to the Chinese academic community. To finishing the cultural project, large number of documents had been collected and analyzed, and about 100 important great physicists had been contacted. A lot of experiencewhich made by Kuhns are worth learning when we do the similar project of culture. Key Words: Thomas Kuhn; Quantum physics; History of science; Sources for history of quantum physics Collaboration Group Size and It. s Impact on the Quality of S. C. C. Ting. s Scientific Performance ) ) ) Based on the Analysis of the Relationship between the Number of Co- authours and the Citation Count of His SCI Papers( p. 56) CHEN Xiao- ling 1. 2 , SUN Yong- jun 3 ( 1. Center for Social Studies of Science, Peking University, Beijing; 2. Beijing Branch, China Railuay Express Co. , Ltd. Beijing; 3. School of Humanities and Social Sciences, University of Science & Technology Beijing, Beijing) Abstract: Throughout his career, Nobel laureate S. C. C. Ting. s co-publications account for nearly 98 percent of all his publications. His collaboration group consists of 400 or 500 members or so, and even more than 2000. The purpose of this paper is to examine the develop- ment trend of T ing. s collaboration group size and it. s impact on the quality of his scientific performance. The findings are: on the whole, Ting. s collaboration group expands with time and reaches a steady state in the later period; the quality of papers improves with the increment of co- authors; Ting. s publication peak is in his most collaborating period; ex cept several classical papers, the quality of most Ting. s papers increases with his age, in which collaboration group size plays a significant role. Key Words: S. C. C. Ting; Collaboration group size; Impact of scientific performance Some Empirical Investigations on / universalism0 by the Mertonian School( p. 64) OU Yang-Feng, XU Meng-qiu ( The Department of Philosophy of Xiamen University, Xiamen, Fujian) Abstract: This article reviews the empirical investigations on / universalism0 by the Mertonian school. The following questions are dis- cussed: the investigations on institutionalized patters of evaluation in science by Merton and Zuckerman; the investigations on peer review at the NSF by Coles; the investigations on the reward systems in Britain and American by Gaston; and the investigations