上世纪70年代，已故数学家Paul Cohen因其在数学逻辑方面取得的成就，荣获得菲尔兹奖(Fields Medal)。Cohen曾做出了一个影响深远的预测：“在未来，数学家将被计算机取代。”这一预测至今仍像梦魇一般萦绕在数学家们的心上，令他们既兴奋，又恼怒。Cohen在集合理论领域的研究方法极其大胆，他还预言：数学领域里的一切都能被自动化，包括数学证明的编写。
证明（proof）是一个循序渐进的逻辑论证，用来验证一个猜想或一个数学命题的真实性。一旦猜想的真实性得到证明，猜想便成为定理。证明的过程既建立论述的效度（validity），又要解释它之所以正确的原因。不过，证明过程是抽象的，不受物质经验的束缚。来自CMU的认知科学家Simon Dedeo专注于通过分析证明结构来研究数学确定性，他说：“证明是意识世界和生物进化物种之间的奇妙联系，但我们不是为了证明才进化的。”虽然计算机利于处理大规模计算，但并不是证明需要的必备条件。猜想来源于归纳推理（inductive reasoning，指的是对感兴趣的问题的直觉），而证明通常是一步步地进行推理。这两者往往需要用到复杂的创造性思维，并需额外人工来填补漏掉的证明步骤，但机器无法做到这一点。机器化的定理证明器可以分为两类：一是自动化定理证明器（Automated theorem provers，ATP），通常使用暴力求解方法（brute-force methods）来处理大量计算；二是交互式定理证明器（Interactive theorem provers，ITP），一般在证明过程中充当辅助工具，协助验证观点的准确性和检查现有证明步骤是否有误。但就算将这两种方法结合起来（就像新的定理证明器一样），也不能实现自动推理。此外，上述的两类证明工具并没有达到大众的期望。许多数学家并不使用这类工具，甚至不待见它们。（图注：Simon Dedeo在解释人与机器进行数学证明的方式是相似的）该领域还存在一个难题：有多少证明是计算机可以自动完成的？计算机系统能否提出一个有趣的猜想，然后用人类能够理解的方式证明它？从世界各地实验室的最新研究进展来看，人工智能工具也许是解决该难题的有效途径。来自布拉格Czech Institute of Informatics, Robotics and Cybernetics的Josef Urban专注于使用机器学习的多种方法来提高现有证明器的效率和性能。今年7月，他的研究团队通报了一组由机器生成并验证的原创猜想和证明。今年6月，来自Google Research的Christian Szegedy及其团队成员发布了一项最新研究成果：他们利用自然语言处理的优点，使机器证明在结构和解释方面更加人性化。一些数学家认为，定理证明器仅仅能够用来训练本科生的证明写作能力。另一些人则认为，对高阶数学来说，用计算机写证明过程不仅毫无意义，也做不到。但Szegedy认为，如果计算机系统能够预测一个有价值的猜想，并证明猜想的有效性、得到新的定理，那么它也一定能取得新突破，比如对机器学习的新理解。由此可见，自动推理是有可能实现的。计算机武艺十八般
数学家、逻辑学家和哲学家一直在争论：在创建证明的过程中，哪些部分必须由人类完成？关于机械化数学的争论也一直持续至今，尤其是在计算机科学和纯数学深度交叉的领域。对计算机科学家来说，定理证明器有利于严格验证一个程序是否有效，找到解决问题的有效方法也比主张直觉与创造力重要。比方说，MIT的计算机科学家Adam Chlipala设计出一些定理证明工具，它们可以生成原本由人类编写的加密算法，以便保护互联网交易的安全性。该团队的算法代码已在谷歌浏览器的大部分通讯工具上使用。Chlipala认为，我们可以使用一种工具对任意数学论据进行编码，然后将论据结合起来，创建安全证明共识机制。在数学领域，定理证明器有利于进行复杂的、计算繁重的证明过程。若没有定理证明器，许多证明过程可能会困扰几代数学家。开普勒猜想便是一个生动的例子。开普勒猜想描述了一种最便于堆叠球体(或橘子、炮弹)的方法。1998年，Thomas Hales和他的学生Sam Ferguson应用了多种计算机数学技术来完成一项证明，但证明结果十分冗长，占用了3g字节，使得12个数学家花了好几年进行详细分析，才只有99%的把握证明这项猜想是正确的。除了开普勒猜想，机器还解决了许多著名的数学问题。比如说四色定理（four-color theorem）。该定理称，只需要具备四种颜色，我们就可以给任意二维地图上色，使得任意两个相邻区域的颜色都不相同。1977年，数学家们使用一个计算机程序，在具有五种颜色的地图上重复验证，结果表明，确实只需要四种颜色即可。再比如2016年，三位数学家用一个计算机程序证明了毕达哥拉斯三元数组问题（Boolean Pythagorean triples problem）。该问题最初的证明过程只有200m字节。得益于高速互联网的连接，人们只需三周多一点的时间就可以把它下载下来。争论不断
上述的成功例子常被人称颂，但也引起了一些争论。早在40年前，用计算机代码证明四色定理便已成既定事实，但人类不可能自己去校验。来自哥伦比亚大学的数学家Michael Harris说：“从那时起，数学家们就一直在争论这是否算是一种证明。”许多数学家，包括Michael Harris本人，都不认为计算机定理证明器是必不可少的，更不认为定理器会淘汰人类数学家。（图注：来自哥伦比亚大学的数学家Michael Harris）另一种反对意见是，如果数学家们想使用定理证明器，他们必须首先学会编程，然后弄清楚如何用计算机可以识别的语言表述他们的问题。这些行为明显不同于数学研究。Harris认为：“等到我把问题都转换为适用于计算机代码的形式，我自己早就把问题解决了。”许多数学家认为定理器对他们的工作来说毫无意义。来自伦敦帝国理工学院的数学家 Kevin Buzzard说：“数学家们也有自己的系统，就是笔和纸，而且还很好用。”三年前，Buzzard将自己的工作重心从纯数学转向了研究定理证明器和形式化证明（formal proof）。Buzzard认为，计算机为人类承担了大规模的计算量，但从未独立解决过任何一个数学难题。只有计算机具备了这个能力，人类数学家才有可能被取代。尽管无惧于计算机威胁论，Buzzard和其他数学家认为，也许他们应该接纳这些证明工具。DeDeo认为，计算机证明可能并不像我们想象的那么神秘。最近，他与斯坦福大学的计算机科学家Scott Viteri一起，对几个著名的经典证明(其中一个取自欧几里得的著作《几何原本》）和几十个由计算机用Coq定理证明器编写的证明进行了逆向工程化，想要找出人类证明与计算机证明的共性。他们发现，机器证明的网络结构与人类证明的结构极为相似，这也许有助于研究人员找到应用证明协助工具进行自我解释的方法。另一些人认为，不论是在计算机科学领域还是数学领域，定理证明器都是有用的教学工具。（图注：约翰·霍普金斯大学的数学家Emily Riehl）来自约翰霍普金斯大学的数学家Emily Riehl开创了一门课程，让课上的学生用定理证明器来写证明过程。她说：“学生在第一次写证明时可能不知道需要用到什么技巧，也很难理解证明过程的逻辑结构，但定理证明器会“逼”你进行条理清晰的思考。”Riehl还提到，她越来越习惯在自己的研究工作中使用定理证明器。她说：“你不需要时时刻刻使用定理证明器，它也永远不能代替用笔在纸上计算的过程，但使用证明协助工具之后，我改变了对书写证明过程的看法。”定理证明器还能保持数学领域的诚实性。1999年，俄裔美国数学家Vladimir Voevodsky在一个证明过程中发现了一个错误。从那时起，他便一直提倡使用计算机来检查证明过程是否有误。Hales也提到，他和Ferguson用计算机检查出了原先证明过程中的数百处错误。即使欧几里得《几何原本》中的第一个命题也不是毫无缺陷的。如果机器能够帮助数学家避免这些错误，为什么不好好利用它呢？(无论合理与否，Harris提出过反对意见：如果数学家花时间将数学转换成计算机能够理解的形式，那就没有时间研究新的数学题了。)（图注：俄裔美国数学家Vladimir Voevodsky）但并非所有的数学家都讨厌定理证明器。来自剑桥大学的数学家兼菲尔兹奖得主Timothy Gowers便想要取得进一步的突破：他希望在未来，定理证明器会取代主要期刊的人类审稿人。他希望未来能形成一个审核标准：投稿论文在通过期刊的审核之前，事先应通过定理证明器的自动检查。数学家如何与计算机交流？
在应用计算机来检查甚至设计证明过程之前，研究人员首先要解决一个难题：克服人类和计算机之间的语言交流障碍。现有的定理证明器并不利于数学家的研究。前面提到的自动化定理证明器（ATP）通常是通过测试所有可能发生的情况，以检查语句是否正确。例如，让ATP验证某个人是否可以从迈阿密开车到西雅图，那么它可能会搜索从迈阿密驶离开往其他所有城市的道路，最终在其中找到通往西雅图的道路。有了ATP，程序员就可以将所有的规则或公理编写成代码，然后检验某个特定的猜想是否符合这些规则。接下来，电脑就会自己完成所有校验工作。正如计算机科学家Daniel Huang所说，你只需输入你想要证明的猜想，然后等待计算机校对的答案。”但问题是：ATP无法解释自己的工作。所有计算过程都是在机器内部进行的，人类只能看到一长串的0和1。Huang说：“我们不可能通过检查这些0和1就搞清楚定理证明器的推理逻辑，因为它们看起来就像一堆随机数。没有人在看到这样的证明过程时敢保证自己看懂了。”第二类交互式定理证明器（ITP）具备大量数据集，其中包含数以万计的定理和证明，ITP可以通过查看这些数据集来验证一个证明是否准确。ATP是在一个黑箱中进行论证后直接给出答案，而ITP需要与人进行交互，人会在证明过程中指导计算机，所以ITP更容易为人们所理解。Huang认为，有了ITP，人们很容易就可以想明白哪些是证明技术。这也是DeDeo和Viteri研究过的证明器。近年来，ITP越来越受欢迎。2017年，来自毕达哥拉斯三元数组的三位数学家使用Coq定理证明器（一种ITP）来创建和验证他们证明的形式化版本。2005年，来自微软剑桥研究院的Georges Gonthier使用Coq将四色定理形式化。在开普勒猜想的形式化证明上，Hales也使用了名为HOL Light和Isabelle的ITP。（“HOL”指的是“higher-order logic”，“高阶逻辑”）该领域的前沿研究尝试将学习与推理结合起来。研究人员通常将ATP和ITP与机器学习工具结合起来，以提高两者的效率。他们设想，ATP或ITP程序可以像人类那样，或以某种类似的方式，进行演绎推理，甚至交流数学思想。计算机推理的局限性
Josef Urban认为，证明方法可以结合演绎推理和归纳推理。他的团队设计了一个由机器学习工具为导向的定理证明器，这样计算机就可以自行从经验中学习。在过去的几年里，他们探索了神经网络的用处。神经网络指的是拥有算力的层数，使用与人类大脑神经活动相似的方法协助计算机处理信息。今年7月，这个研究团队报告了一个基于定理证明数据训练的神经网络生成的新猜想。Urban的部分灵感来源于Andrej Karpathy在几年前训练了一个神经网络来生成一些看起来与数学有关、但实际上毫无作用的内容（外行人看起来可能有用）。但Urban并不想搞这些没用的东西。在训练了上百万个定理后，他和他的团队设计了自己的神经网络来寻找新的证明，然后利用这个网络生成新的猜想，并使用一个名为E的ATP检验这些猜想的有效性。这个神经网络提出超过5万个新公式，虽然其中有上万个是复制来的，还没有能力提出更有趣的猜想。 Google Research的Szegedy认为，计算机证明中的自动化推理难题只是NLP领域里的一小部分，涉及到使用单词和句子进行模式识别。模式识别也是驱动CV发展的一个方法，而CV正是Szegedy在谷歌的之前研究项目的目标。与其他团队一样，他的团队也想获得能找到并解释有用证明的定理证明器。有感于人工智能工具的快速发展，比如由DeepMind公司开发的AlphaZero在国际象棋、围棋、shogi（日本象棋）等游戏中战胜人类，Szegedy的团队希望利用语言识别的最新成果来编写证明。Szegedy认为，语言模型展示了惊人的数学推理能力。近日，Szegedy在Google Research的团队使用语言模型(通常是使用神经网络)来生成新的证明。他们首先训练模型来识别定理中一种已知是正确的树状结构，接着进行了一种自由变形（free-form）的实验，让网络无需进一步的指示自动生成并证明一个定理。在数千个网络生成的猜想中，大约13%是可证明的、新的猜想，也就是说，它们不是通过复制数据库中的其他定理得来的。Szegedy认为，这个实验表明了，神经网络可以自学理解证明是什么样的。Szegedy认为，神经网络能够发展出一种人造直觉。当然，目前还不清楚他们所设计的神经网络是否会实现科恩40多年前的预言。Gowers认为，到2099年，计算机在推理方面将会超越数学家。他预言，一开始数学家会享受这种黄金时代：有趣的工作由数学家来做，无聊的工作则由计算机完成，但这只会持续很短时间。因为如果计算机的能力不断提升，还可以访问大量的数据，那么计算机也会越来越擅长执行有趣的工作，并学会如何一步步提升自己。Harris不同意Gowers的上述观点。他认为计算机证明器不是必要的，也不会取代人类数学家。即使计算机有能力编写出一种合成直觉程序，它仍然无法与人类的直觉合成机制相媲美，因为就算计算机有“理解能力”，它们也无法像人类一样去理解。https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/
在AI科技评论9月11日推文“《柏拉图与技术呆子》：探讨人类与技术的创造性伙伴关系”留言区留言，谈一谈你对本书的相关看法、期待等。
AI 科技评论将会在留言区选出5名读者，每人送出《柏拉图与技术呆子》一本。
活动规则：
1. 在留言区留言，留言点赞最高且留言质量较高的前 5 位读者将获得赠书。获得赠书的读者请联系 AI 科技评论客服（aitechreview）。
2. 留言内容和留言质量会有筛选，例如“选我上去”等内容将不会被筛选，亦不会中奖。
3. 本活动时间为2020年9月11日 - 2020年9月18日（23:00），活动推送内仅允许中奖一次。
