姓名:王紫圣    学号:16130140355

转载自:武汉 华中师范大学国家数字化学习工程技术研究中心  430079

【嵌牛导读】 计算机是数学家们自豪的发明，而计算机也在潜移默化的影响数学

【嵌牛鼻子】计算机和数学

【嵌牛提问】计算机能否推理？

【嵌牛正文】人不是机器。

这句俗语通常是用来说明人需要休息，而机器则可以不眠不休地干下去。

把繁琐沉重的活交给机器，人可以解放出来做更灵巧的富于创造性的工作。体力劳动如此，计算机出现后脑力劳动亦如此。

计算机科学技术迅速发展，机器的智能化程度越来越高。但你要和谁说，计算机能解数学题，而且所给解法和人给出的解法相似或更简洁优美，这是很难让人相信的。世界上研究机器推理的一流学者，曾经普遍认为这是不可能的。

因为推理是人独有的高级智慧。

人通过推理，可以由此及彼，由表及里，去粗取精，去伪存真。

那么人能不能把这智慧赋予给计算机呢？

计算机是人的学生。它的本领是人教的。它是笨学生，不教不会。但它又是好学生，会牢牢记住你教给它的方法，一丝不苟地按你写好的程序去做。如果你循循善诱，它就能青出于蓝。

计算机的发展，特别是机器证明的出现，给数学和哲学带来的影响是巨大而深刻的。

就拿中学数学来说吧。初中数学大致分为代数和几何两部分。代数问题的求解通常是比较规范的，按照一定的步骤依葫芦画瓢即可，关键是计算不出错；而几何则不同，难度稍大的题目，往往无从下手，好似羚羊挂角，无迹可寻。辅助线从何而来，要么是妙手偶得之，要么是千锤百炼得来。正因为如此，当古代托勒密王向欧几里德请教学习几何的捷径时，欧几里德直率地说：几何无王者之路!

计算机的发明，是为计算而来，这从它的名字就可以充分说明。不管计算机将来如何发展，如何智能化，高速的计算能力始终是计算机的根本。

为计算而发明的计算机，能够证明几何定理么？中国数学家在上个世纪80年代提出的例证法算是一种，因为计算量很大，大多数情况只能借助计算机来完成。除此之外，还有别的什么方法吗？答案是肯定的。用机器证明的数学定理中，最为人津津乐道的当属四色定理。

1四色定理的机器证明

四色定理最先是由一位叫古德里的英国大学生提出来的。德·摩尔根1852年10月23日致哈密顿的一封信提供了有关四色定理来源的最原始的记载。他在信中简述了自己证明四色定理的设想与感受。

四色问题的内容是：“任何一张地图只用四种颜色就能使具有共同边界的国家着上不同的颜色。”用数学语言表示，即“将平面任意地细分为不相重叠的区域，每一个区域总可以用1、2、3、4这四个数字之一来标记，而不会使相邻的两个区域有相同的数字。”

100多年以来，数学家们为证明这条定理绞尽脑汁，所引进的概念与方法刺激了拓扑学与图论的发展，但一直没有得出证明。

1976年，美国数学家阿佩尔与哈肯借助电子计算机，用了1200个小时，作了上百亿次判断，终于完成了四色定理的证明，轰动全世界。美国为此发行一枚纪念邮票，上面写着“四种颜色就够了”。

当一些数学家为一个高难度的定理得到解决而庆祝时，更多的数学家是对计算机给出的证明表示质疑。质疑的理由有二：

一是对于相当多的定理证明，特别是那些被称为“下金蛋”的数学问题，最重要的意义不在于论证最终的真假，而是在求证过程中不断的发现新方法。

二是计算机凭借高速计算能力作出的所谓证明，数学家无法人工检验，谁知道中间会不会出错呢?

新事物的产生和发展，往往不是一帆风顺的。

在计算机还没发明的时候，就有数学家提出机器证明（设计一种机器代替人推理）的设想，遭到了很多数学家的反对。数学大师庞加莱认为：“你可以将牲畜赶到机器的前端，机器将其宰杀后储存成罐头输出。难道你可以把定理的条件送到机器的前端，机器自动输出结论么？这实在是不可思议！”

而在四色定理机器证明之后，反对声仍然强烈。有评论认为:机器证明破坏了数学的优美。一个好的数学证明应当像一首诗——而这纯粹是一本电话簿！”

普林斯顿数学教授约翰•康威在接受《纽约时报》采访时说:“我不喜欢它们（计算机证明），因为你感觉不知道究竟发生了什么。你不能从中获得任何新的见地。”

持这种观点的数学家不是个别的，他们认为：如果一个难题被一种新方法解决了，这是一件了不起的事情。但是如果解决的方案只是现存方法的反复使用，那只能证明解决者的聪明而已。这不利于数学的发展。

还有人指出:传统数学研究四色定理，虽未获得最终成功，但促进了某些数学分支的发展(主要是图论、拓扑等)；而机器证明四色定理结论是对的，又能咋样呢?只得到没有灵魂的空壳而已。因为四色定理本身的意义并不大。现在数学界普遍承认五色定理了， 但世界上绝大多数的地图颜色都超过5种。因为除了考虑颜色种类最少，现实生活中还有其他的考虑。

但是，机器证明四色定理毕竟丰富了我们的知识。以不能产生新方法为理由就拒绝承认，是说不过去的。用机器作为数学研究的辅助工具，这本身就是新的方法。

从历史上看，工具对数学的发展有重大的影响。筹算和珠算无疑推进了位置记数法和相应的计算系统的发展；圆规和直尺的使用不但推动了几何作图的研究，对近世代数的产生也有深远影响。计算机能够计算，能够作图，也应当能够推理。事实上，在计算机出现之前，数学家已经论证了推理化为计算的可能。

计算机的能力远远超过筹算、珠算、圆规和直尺的总和。数学家有了这样强大的工具，数学的面貌自然会有深刻的变化。

2 计算机证明的定理可靠吗？

机器证明是否可靠，如何检验，这确实是一个问题。

不过，人工证明也要面对这个问题。

当代的数学有些已经很复杂。有些数学定理的证明超过百页，这使得审稿成为异常艰辛的工作。

以代数中著名的有限单群分类定理为例。确切来说，这不是一个定理而是一组定理。它的证明由五百篇论文组成，总页数超过一万页。世界上恐怕没有人认真地把这个证明从头到尾读过，更别说验证其正确性了。这样冗长的证明使不少数学家怀疑其中会有错误。对此，在该定理的最后证明中起重要作用的Aschbacher评论道：“一方面，当证明长度增加时，错误的概率也增加了。在分类定理中出现错误的概率实际上是1。但是另一方面，任何单个错误不能被容易地改正的概率是0。随着时间的推移，我们将会有机会推敲证明，对他的信任度必定会增加。”

前苏联数学家彼得洛夫斯基院士，在常微分方程定性理论方面有一个著名的结果。在多年后被中国的一位研究生用反例推翻了。

前苏联另一位专家关于钢管校直机械有一个著名公式，这公式写入了教科书，获得过国家大奖。中国的一位技术员在实践中发现按此公式设计的苏联设备废品率偏高，向一位数学教师请教，最后发现了这公式推导中有错，终于改进了机器的设计而获得好的效果。这位技术员因此获得国家发明一等奖。

人工证明都会出错且难以检验，又何必苛求计算机呢？

何况，计算机科学已经证明，有些定理即使最短的证明也会很长很长。例如，可以超过十万页，也可以超过百万页。

尽管如此，大家还是希望计算机能够干得更出色，更可信。

计算机得出的结果，有些是容易检验，容易相信的。

例如，把某一个很大的整数分解为两个大于1的整数的乘积，这是破解一类密码的关键任务。大型高速计算机工作几个月才分解了一个整数，人只要几分钟就能检验结果是否正确。

类似的，计算机算出来的方程的解是否正确，也不难检验。

但定理证明是另一回事。在例证法中，面对计算机用十万个例子证明了的一条几何定理，我们会有什么想法？

与此类似，用代数方法经过成百上千项的多项式计算而证明的几何定理，我们会有什么想法？

我们可以相信这条被计算机宣布成立的定理。前提是计算机的硬件是可靠的，计算机的操作系统是可靠的，机器证明软件的程序是可靠的，程序依据的算法和理论是可靠的。

算法和理论的可靠性，通过学习和讨论，不难确认。

其他几种可靠性，可以经过大量实践验证。

譬如让另外一批人，用另外的算法编程，用另外的机器运行，假如推导出来的结论与之一致，那么可靠性得到了增强。因为一个定理，反映一个客观事实。这个事实不会因发现的人的不同而改变，同样也不会因为证明程序的不同而改变。

这样做，从哲学上看，是不是改变了数学真理的性质呢？

另一种方法，是计算机给出人工能够检验的证明。

1976年，吴文俊院士发表了检验几何命题的有效地机械化方法。吴法的成功激起了几何定理机器证明的研究热潮。到1992年，基于几何不变量的消点方法出现，实现了几何定理可读证明在计算机上的自动生成。这一工作被国际同行誉为计算机处理几何问题的里程碑。

伴随着计算机技术的进步，直到1996年出现了基于前推模式的 “几何信息搜索系统”，成功地证明了上百个非平凡的几何命题，收到了良好的效果。

人们对机器证明的反对，多半集中于它的繁琐和不可检验。一位反对机器证明的数学家说:数学的光荣，便在于它现有的一切证明方法，都是脉络绵密，层次分明，就像天衣无缝，出不了差错的。而使用计算机则有可能出现人无法检验出来的差错，而这差错可能是致命的。

现在已经实现的几何定理可读机器求解，所生成的解答其推理过程的简洁优美可以与人工解答媲美。虽然解决的只是一小类数学问题，远没有达到解决四色定理、哥德巴赫猜想一类难题的水平，但至少说明了机器证明和人工证明之间并没有不可逾越的鸿沟。人类的创造力再一次得到展现。

国外还出现一些人机交互的计算机推理系统，如Coq、Otter、Roo等等。借助这些系统，能够用来进行不同的数学领域的推理，所生成的证明类似于数学家的工作。

对于人类面临的很多难题，既然单个群体无法解决，那我们齐心协力一起解决不是很好么？数学家提供理论基础，计算机科学家设计算法并编程实现，而物理学家和工程师们则要保证计算机本身的稳定性。

我们坚信，机器证明不但不会像有些数学家担心的那样“使数学走向衰败”，还将使数学家摆脱大量的繁琐的机械计算和推理，把节省下来的时间和精力用于更加富有创造性的工作中去。

3数学和计算机共同发展

数学和计算机都在以前所未有的速度发展着。

计算机的出现，改变着数学家的工作方法，提高了数学家工作的效率。数学家把大量机械性重复性的劳动交给计算机，自己可以从事更抽象更富于创新精神的思考。计算机计算作图的结果，增强了数学家的预见能力，引导数学家发现有意义的问题和现象。

计算机的出现，促使新的数学分支的诞生。计算数学、计算几何、计算机代数、计算复杂性、计算可靠性、机器证明、计算机作图、动态几何……等等与计算机血肉相连的分支应运而生。有些分支在学科上表面已经归于计算机科学，其本质上仍是数学。

计算机的出现，开始改变着人们对数学的看法。出现了数学实验和实验数学。用计算机做实验，发现了大量有趣的数学现象，如分形、混沌、分岔等许多过去想到看不到或者想也想不到的东西。这些东西使数学家大伤脑筋又大开眼界。有人惊呼，数学越来越像实验科学了。

计算机科学就好比是数学科学的孩子。虽然这个孩子长大了，搬出去住了，但身上始终流着母亲的血液，仍然从母亲这里吸取着养料。

数学也并没有白养这个孩子。在计算机产生和发展的过程中，数学也同时得到发展。而在计算机发展成熟之后，推动着数学飞速的向前。计算机成为数学研究的工具已是大势所趋，不可阻挡了。

计算机一直被认为是数学家最引以为豪的发明。既然现在最好的计算机可以在比赛中打败世界象棋冠军，那么，有理由相信未来的计算机也应该能够解出难倒了最伟大的数学家的数学难题。倘真的有那么一天，母亲绝不会因为孩子的超越而郁闷，而是会为孩子的成就由衷地高兴。

我们甚至可以设想到了那一天， 每一个数学家都是计算机高手，而机器证明和人工证明也可以很好地转化；当数学家向杂志投稿时，审稿人会问:你的证明经过计算机验证了吗?

那时候，莱布尼茨之梦才算真正实现。数学从此有了王者之路!

注：莱布尼茨之梦——1673 年，27 岁的莱布尼茨向人们展示了一台能够执行四种算术基本运算的计算机模型。对这位年轻人来说，这只是迈出的一小步。自青年时期开始，具有宏大而惊人眼光的莱布尼茨脑中就产生了一个奇思妙想：创造一种“普遍文字”，能够把人类的思想还原为计算，并且制造出强大的机器能执行这些计算。这意味着人类可以通过“让它算一下”的方式一劳永逸地解决几乎所有问题。何等宏伟的梦想！