数学家可以被计算机取代吗？

科学无国界，我们是知识的搬运工

作者：Marianne Freiberger and RachelThomas 翻译：Nothing 审校：loulou

数学家将来会被计算机代替吗？如果数学只包含程序化的计算，那么答案是肯定的。但是如果你想让计算机进行数学证明，甚至解决逻辑上的难题，你也知道这样的问题需要直觉和想象力的跳跃，这是计算机的能力之外的事情。即使仅仅是判断哪种问题在数学上是有趣的、无聊的或者无法研究的，貌似也不得不让人参与其中。

在B(A)管理委员会就“证明的未来”进行辩论的小组。

计算机辅助的证明

依靠计算机的辅助来进行证明并不是新鲜的事情。第一个例子就是1976年对四色定理的证明，四色定理是指任何一个画在平面上的地图仅需要四种颜色，就足以保证任意两个相邻的国家可以用不同的颜色标注。为了证明这个说法，计算机检验了大量的地图从而证明了这个定理的正确性。1998年著名的开普勒猜想，它指的是如何堆积一些圆球使得它们占据的空间最小，对这个猜想的证明我们更多的借助于计算机。

使用四种颜色上色的地图

这些证明隐含着一个问题：没有一个人能够检查计算机是否出错。一些人会反对说，这样的证明不能被认为是完全证明，但是其他人愿意接受这些由机器辅助完成的证明。正如Barrow-Green指出的，单个数学家不能完成的证明不一定非要计算机的辅助才能完成：一个例子是100多位数学家共同努力完成了对有限简单群的分类。当然计算机的使用也不是一件新鲜事。Martin引用了Hardy和Ramanujan的例子，他们在二十世纪初用MajorMacMahon计算得到的表格来研究分拆函数（partition function）。

计算机做出的证明

计算机还可能以一种更加神奇的方式帮助数学研究。Automated theoremprovers（ATPs）是一种可以利用逻辑规则产生数学结果的程序：它能得到一个可以从假设和公理出发并按照逻辑推理得到的结果。

ATPs已经在数学中获得一些成功，但有趣的是，它在我们的生活中也产生了影响。计算机程序在广泛的领域内都得到了应用，从控制客机或核反应堆到心脏起搏器。为了安全和节省资金，你需要知道这样的系统是否工作正常。确保这一点的一种方法是在大量情景下多次测试一个系统，并确保它总是做正确的事情——但这可能会耗费大量时间，更要命的是，如果不能测试所有可能的情况，测试可能仍然会错过发现错误的机会。相反，我们可以使用ATPs，以数学方式验证特定硬件系统或运行在其上的代码是否正确，并始终按其应该的方式运行。

ATPs仍然需要大量的人工输入来工作，但Pitts相信，至少在计算机科学中它正引起巨大的变化。许多数学家可能会觉得这种发展有点悲哀：正如Pitts指出的，这意味着人们不再关心如何使数学论证变得优雅。计算机不关心是否使用暴力求解的手段得到证据，例如遍历检查所有的可能性——其目的只是为了找到一个证明。相比之下，人类数学家总是想寻找一个更高层次的原理，可以将所有这些可能性统一在一个优雅的过程中。事实上，在计算机科学中所做的证明通常是“又大又丑”。

真的不需要人类吗 ？

但是，也许这些发展并不需要过多地关注数学家;毕竟，它们只是数学在不同领域的应用。但Gowers相信，即使是在数学领域内伟大的事情仍然会到来。人类数学家与计算机的区别不仅仅在于他们喜欢让证明变得优雅美丽，他们也希望能提供一些关于结果为什么真实可靠的看法。他们发现证明似乎是人类独有的思考方式，例如不同领域的数学以及数学和科学之间可以在更高的层次产生联系，而目前的计算机显然是不可能做到这一点的。

但是Gowers认为，即使在人类使用的数学方法中，证明也不是完全抽象的。如果我们能真正理解我们所说的“证明”到底是什么意思，人们如何发现证明，并创建一个将现有的数学知识合理分类的数据库作为背景知识，那么也许有一天我们能让计算机证明像人类数学家一样进行证明。

Gowers认为，到本世纪末，人类数学家很有可能真的将自己从证明中解放出来。一旦计算机能够很好地证明一些结果，它们也就能够很好地决定要证明哪些结果，从而完全摆脱了人类的指导。

如果你熟悉哲学，那么一个反对的声音会立刻浮现在你的脑海中。计算机除了使用公理化的数学方法别无选择。他们的逻辑推断需要基于一套公理和规则，你可能质疑这些公理和规则应该是什么。更重要的是，库尔特·哥德尔在20世纪30年代证明了任何一个形式系统，只要包括了简单的初等数论描述，而且是自洽的，它必定包含某些系统内所允许的方法既不能证明真也不能证伪的命题。

这似乎限制了计算机作为数学家的能力，但如果你仔细想想，人类数学家面临着同样的限制。面对这些问题，我们仍然在做数学，大多数数学家就算有也只会在休息日担心这些基础问题。如果计算机变得像Gowers所说的那样优秀，那么也许有一天他们能够自己去思考这些问题。

数学中的合作

关于有限单群分类的工作涉及一百多位数学家的共同工作。

除了计算机之外，还有另一种技术影响我们研究数学的方式。正如Barrow-Green指出的，数学从来不是一个人单打独斗的工作。几千年来，我们的证明标准发生了变化，因此人们不断地重新审视得到的结果，提出新的证明和看待它们的新方法。如今，技术使人们可以同时为一个结果进行集体工作。这些协作证明的一个例子是上面提到的有限单群的分类，它于2004年完成，涉及了遍布世界各地的100多名数学家——这在纸质信件的时代肯定是不可能实现的。另一个例子是Gowers建立的polymather项目，它允许数学家通过在线发布他们对问题的想法或评论他人的想法进行合作。

Tranah认为，这种发展应该会改变数学审查和出版的本质。目前，数学家们把他们的论文寄给学术期刊，由该领域的其他专家对其进行审查，如果这些专家认为结果正确且有趣，他们就发表论文。这些期刊充当的是数学成果的记录员，并且充当了你在查找时要去的“图书馆”。

Tranah认为，如今，这些期刊只不过是“垃圾邮件”，作为他们工作的记录，实际上只对论文作者及其机构有益。当数学家们寻找新的结果时，他们不会等待可能长达数年的论文审查期。相反，他们会选择论文预印本网站，在正式发表论文之前，这些服务器会发布论文，并使用数学家的声誉和他们自己的专业知识来评估论文的价值。因此，传统的同行评审过程可能会被群体评审过程所取代。有趣的论文将吸引许多数学家的在线关注，随着时间的推移，他们将在论文中添加更正和评论。这样的过程将把好论文和坏论文分开，并确保它们是正确的。出版商将不再需要麻烦同行评论，从而节省时间和金钱。

解释和真相

了解如何建立证明对每个人都至关重要。计算机科学家需要这些信息，以便他们能够创建更强大的自动化系统。历史学家和哲学家正在尝试洞察数学文化，以及寻找在数学界被认为有效的东西。数学家们想学习如何研究更多的数学。理解想法是如何建立起来的正是我们和朋友喝咖啡的时候所讨论的事。这比学术文献中出现的最后的证明要有力得多，我们几乎不知道这些证明是如何被发现的。

这场辩论的核心问题是：什么是证明？它们仅仅是真理的证明，还是应该揭示某些事情是真实的？对于许多数学家来说，解释事物真实性的证明最有价值。这种证明能用计算机实现吗？

原文来源：

https://plus.maths.org/content/future-proof

互动问题

【互动问题：你觉得什么是证明？】

欢迎在评论区留言。

编辑：loulou