计算机算出来的数学证明

Python与开源GIS

计算机算出来的数学证明

2016-11-08 作者: xuzhiping 浏览: 4284 次

摘要: 1998年8月,黑尔斯给数十位数学家寄去了电子邮件,宣布他已经利用计算机证明了400年来一直无法确认的猜想。那封电子邮件的内容是对德国天文学家开普勒提出的开普勒猜想的证明: 球体最紧密的排列方式就是金字塔般的堆栈方式,类似杂货店堆橙子的方式。黑尔斯宣告证明成功...

1998年8月,黑尔斯给数十位数学家寄去了电子邮件,宣布他已经利用计算机证明了400年来一直无法确认的猜想。那封电子邮件的内容是对德国天文学家开普勒提出的开普勒猜想的证明: 球体最紧密的排列方式就是金字塔般的堆栈方式,类似杂货店堆橙子的方式。黑尔斯宣告证明成功后不久,全球报纸的头版都刊登了这项突破,但黑尔斯的证明还是无法被完全肯定。他将这份证明投到声誉卓著的《数学年刊》,却未获正式刊登。负责审稿的人表示,虽然他们相信这证明是正确的,但他们缺乏可以验证的程序来确保排除任何可能的错误。因此,最终出现在年刊上的是黑尔斯的手稿,并附上一则罕见的编辑附注,声明这篇论文的部分内容无法审查。

这个超乎寻常的故事的问题核心是“计算机在数学上的应用”,事实上,各方对这个一体的看法两级化。通过计算机辅助的证明结果有时被形容为“暴力”解法,通常必须在计算了成千上万个可能的结果后,才会得到最后的答案。许多数学家不喜欢这种方法,认为过于粗野,其他人则批评这种做法对理解正在探讨的问题毫无帮助。例如,1977年有人宣布利用计算机辅助,证明了四色定理。所谓四色定理,是指假设我们想要用不同颜色来填满地图,并且满足相邻区域的颜色均不同的条件时,只需要四种颜色。虽然无法从证明中找出任何错误,但有些数学家还是坚持继续运用传统的方式来寻找答案。

黑尔斯转到宾州匹兹堡大学之前,已经在安阿伯密歇根大学研究了这项证明。一开始,他先降低可能的堆栈方式种数,从无限多种减少到5000种左右,然后再用计算机来计算每种排列方式的密度。这项工作听起来简单做起来难,证明过程包括用专门编写的计算机程序来检验一系列数学不等式,而10年内总共检验了超过10万多条不等式。新泽西州普林斯顿高等研究院的数学家麦克弗森,同时也是《数学年刊》编辑之一,在听到这 个证明时觉得很好奇,要求黑尔斯及协助证明的研究生弗格森先将他们的发现投稿出版,但同时他对计算机辅助研究这件事也感到不安。

《数学年刊》之前也曾收到过一篇篇幅较短的拓扑学相关文章,那篇文章也是利用计算机辅助证明。麦克弗森在试探过期刊编辑委员会同事的意向后,请黑尔斯寄出论文,这次他一反常态,指派了12位数学家来审核这个证明(大多数期刊的评审只有1-3位)。匈牙利布达佩斯的阿尔弗雷德.雷尼数学研究院的加博尔.费耶什•托特负责带领这个审核小组,他的父亲数学家拉斯洛•费耶什•托特在1965年曾预测,有一天计算机将使证明开普勒猜想成为可能。评审着不仅要重新运行黑尔斯的计算机程序,还必须检验程序是否按照设想的步骤工作,由于计算机代码及输入、输出数据总共占了3000兆位内存空间,评审无法一一检验,所以他们的审核方式限于检验一致性,重新建构每个证明步骤的思考过程,以及研究用来设计计算机程序的所有假设及逻辑。他们在一学年中举办了一系列研讨会,协助进行这项工作。

即使如此,仍难以确认黑尔斯已经成功证明了开普勒猜想。2002年7月,托特报告说,他及其他评审者以99%的确定性认为这项证明是合理的。他们找不出错误或疏忽,但又觉得因为没有一行行检查过计算机程序,所以仍然无法完全肯定这项证明是正确的。

对一个数学证明来说,这还不够。毕竟大多数数学家早已相信这个猜想,该证明应该把相信转变为确定,而且开普勒猜想的历史也让人对这项证明抱持谨慎的态度。1993年,加州大学柏克莱分校的项武义在《国际数学期刊》上发表了长达100页的猜想证明;但发表后不久,就被找出证明中的错误。虽然项武义坚信自己论文的正确性,但大多数数学家都不相信他的证明成立。

评审报告出炉之后,黑尔斯说他收到了麦克弗森的一封来信:“我个人认为,评审的决定不乐观。他们现在无法证实证明的正确性,将来也一样,因为他们已经精疲力竭……如果他们一开始有较为清楚的原稿,我们就可以预测他们的审核过程是否能够得到明确的结论,不过现在都无所谓了。”

最后一句话透露出麦克弗森的不满,因为黑尔斯提交的证明并不是一篇严谨的著作,250页的手稿是由5篇独立的论文组成,而且黑尔斯和弗格森在每篇论文中塞满计算机计算出来的证明结果,看起来反而有点类似实验报告。这种反常的格式很难阅读,更糟的是,各篇论文中的附注与定义也略有不同。

麦克弗森要求作者必须编辑他们的手稿,但黑尔斯和弗格森不想再花一年时间重新处理这篇文章。“黑尔斯可以用余生来简化这个证明。”弗格森在完成他们的论文后说道,“但那不是合理利用时间的方式。”

黑尔斯已经开始接受另一项挑战,他想以传统方式来解答有2000年历史的蜂巢猜想: 用相同面积的瓷砖来铺满地面且不留缝隙时,六角形瓷砖的周长最短。弗格森离开了学术界,到美国国防部任职。

面对累坏了的评审,年刊的编辑委员会决定刊登这篇论文,但前提是谨慎地加上附注。文章开头有编辑引言,声明此类以计算机验证大量数学式的证明,可能无法完整检验。整个事件原本可以就此结束,但黑尔斯无法接受他的证明被加上这种附注。

2004年1月,他展开了 “开普勒的正式证明”计划,简称FPK,不久又被昵称为“小斑”。这次黑尔斯不再仰仗人类的评审,他要用计算机验证证明的每一个步骤,这项工程大约需要10位志愿者组成团体来共同研究,这些人必须是乐意贡献计算机时间的合格数学家。团队将撰写程序,把证明的每一个步骤,一行接着一行地拆解成一组已知成立的公理。如果程序的每个部分都可以分解成这些公理,最后就可以确认这个证明是正确的,而参与者也不仅仅将该计划视为黑尔斯证明的验证。

自愿参与这项验证计划的纽约大学研究生麦克劳林曾接受过黑尔斯的指导,也曾使用计算机解过其他数学问题。“以人力来检验计算机辅助的证明,几乎是不可能的。”他说道,“幸运的话,我们将显示这类规模的问题无需通过评审流程,就可以严密地验证。”但不是每个人都像麦克劳林那么热心。高等研究院代数几何学家德利捏是众多不认可计算机辅助证明的数学家之一。他表示我只相信我了解的证明。”对那些与德利涅站在同一阵线的人而言,以计算机取代评审流程的人力审查是错误的步骤。

虽然对证明方式采取保留态度,麦克弗森并不认为数学家应该脱离计算机。荷兰奈梅恩天主教大学的魏迪克是用计算机来验证证明的先驱,他认为这项程序可以变成数学界的标准惯例。魏迪克说,“将来人们会回顾20世纪与21世纪之交的时候,然后说‘就是从那时候开始的’。” 无论计算机验证是否已经广泛被使用,“小斑”要产生结果可能都还要几年。虽然其他人也表达了参与计划的兴趣,但确定的参与成员仅黑尔斯和麦克劳林两人。黑尔斯估计,从撰写程序到执行程序的整个流程,可能需要20个的工作。届时开普勒猜想才会成为开普勒定理,我们也才能确定这些年来一直堆橙子的方式是正确的。

关注“开源集思”公众号
获取免费资源

随机推荐


Copyright © from 2014. 开源地理空间基金会中文分会 吉ICP备05002032号

Powered by TorCMS

OSGeo 中国中心 邮件列表

问题讨论 : 要订阅或者退订列表,请点击 订阅

发言 : 请写信给: osgeo-china@lists.osgeo.org