人工智能工具包定义了下一代自动定理证明者的形状，并由此定义了数学和机器之间的关系。
据说在1970年，已故的数学家保罗·科恩（Paul Cohen）是他在数学逻辑方面的工作获得菲尔兹奖的唯一得主，他做出了毫无根据的预测，这一预测仍然使数学家感到高兴或恼火：“总有一天，数学家将取代未来电脑 ”。科恩以在集合论中的大胆研究方法而闻名，他预测所有数学都可以自动化，包括编写证明。
证明是一步一步的逻辑推理，可证实假设或数学假设的真实性。证明出现后，假设便成为一个定理。它既可以确认该声明的正确性，又可以解释其正确性的原因。但是证明很奇怪。它是抽象的，与物质经验无关。卡内基·梅隆大学的认知科学家西蒙·狄德奥（Simon Dedeo）说：“它们是虚构的非物质世界与生物进化产生的动物之间疯狂接触的结果，他通过证据结构分析研究数学确定性。 “进化并没有为此做好准备。”
计算机适合于大容量计算，但证明要求有所不同。假设来自归纳推理-与一个有趣的问题相关的特殊直觉-证明通常遵循演绎的逐步逻辑。他们通常需要复杂的创造性思维以及填补空白的艰苦工作，而机器无法处理这种技能组合。
计算机定理证明可分为两类。自动化定理证明者（ATP）通常使用蛮力方法来研磨大量数字。交互式定理证明者（ITP）充当人工助手，并且能够检查参数的准确性，以及查找现有证明中的错误。但是，即使您将这两种策略结合在一起（更多现代证明也是如此），自动推理系统也不会从它们中出现。
卡内基梅隆大学的认知科学家西蒙·德迪奥（Simon Dedeo）帮助证明了人类和机器以类似的方式创建了数学证明。
另外，这些工具很少有人欢迎，大多数数学家都不使用或认可它们。 Dedeo说：“对于数学家来说，这是一个有争议的话题。” “大多数人不喜欢这个主意。”
这个领域的开放性难题之一是可以自动执行多少个证明创建过程的问题。系统是否能够产生有趣的假设并以人们可以理解的方式证明它？全球实验室的一系列最新突破提供了人工智能（AI）的方式来回答这个问题。布拉格的捷克信息学，机器人学和控制论研究所的约瑟夫·厄本（Joseph Urban）正在探索各种使用机器学习来提高现有证明者有效性的方法。在七月，他的小组显示了由机器创建和验证的一组原始假设和证据。 6月，由克里斯蒂安·塞格迪（Christian Szegedi）领导的Google Research小组发布了尝试结果，这些结果试图利用自然语言处理系统的优势来使计算机证据的结构和解释与人类的证据更加相似。
一些数学家认为定理证明是可以改变学生学习写证明方式的工具。其他人则说，即使不是不可能，也不必让计算机为高级数学编写证明。但是，一个可以预测有用假设并证明新定理的系统可以实现新的东西-一种理解的机器版本，Szegedi说。这暗示了自动推理的可能性。
有用的机器
数学家，逻辑学家和哲学家们长期以来一直在争论证明的本质是人类的哪一部分，关于数学机械化的争论今天仍在继续，尤其是在计算机科学与纯数学合并的情况下。
对于计算机科学家来说，定理证明没有争议。它们提供了一种清晰的方法来证明该程序正在运行，关于直觉和创造力的争论不如找到解决问题的有效方法重要。例如，亚当Chlipala，计算机科学家在麻省理工学院，先后开发定理证明工具生成保护互联网交易的加密算法-尽管通常人们会想出这样的算法。他的群组代码已在Google Chrome浏览器中的大多数通信中使用。
约翰·霍普金斯大学的Emily Riel使用定理证明来训练学生和计算机助手。
Chlipala说：“您可以采用任何数学陈述并使用一种工具对其进行编码，然后结合所有参数并获得安全性证明。”
在数学中，定理证明者帮助产生了复杂且计算量大的证明，否则将花费数以千计的数学人年。一个明显的例子是开普勒的假设关于三维空间中最密集的球堆积（从历史上讲，它们是橙子或炮弹）。 1998年，托马斯·海尔斯（Thomas Hales）和他的学生山姆·弗格森（Sam Ferguson）使用多种计算机数学技术完成了这一证明。结果是如此繁琐-证明占用了3 GB-使得12位数学家对它进行了数年的分析，然后才宣布他们对它的真实性有99％的把握。
开普勒的假设并不是机器解决的唯一著名问题。与四色定理1977年，他使用一种计算机程序处理了五色地图，并指出可以将所有四种颜色转换成四色。2016年，三位数学家使用计算机程序来证明毕达哥拉斯三胞胎的长期布尔问题，但该证明的第一版为200 TB。如果您有足够快的Internet连接，则可以在三周内下载它。
五味杂陈
这些例子经常被吹捧为成功的例子，但它们也增加了自己的争议性。 40多年前证明四色定理的计算机代码无法被人类验证。哥伦比亚大学的数学家迈克尔·哈里斯说：“从那以后，数学家们一直在争论这是否成立。”
许多数学家与哥伦比亚大学的迈克尔·哈里斯（Michael Harris）一起质疑是否需要创建计算机化的定理证明，而后者将使数学家不必要。
数学家的另一个不满是与以下事实有关：如果他们想使用定理证明，他们首先需要学习如何编程，然后想出如何用计算机可理解的语言来表达他们的问题，而这一切都分散了数学的注意力。哈里斯说：“当我以适合这项技术的方式重新提出问题时，我会自己解决这个问题。”
许多人根本不认为需要定理求解器。凯文·巴扎德（Kevin Buzzard）说：“他们有自己的系统，铅笔和纸，而且可以使用。”是伦敦帝国理工学院的数学家，三年前将研究方向从纯粹的数学转变为定理证明和形式证明。他说：“计算机为我们做出了惊人的计算，但他们从来没有独自解决难题。” “而且直到那件事发生之前，数学家不会买它。”
但是Buzzard和其他人认为，他们可能仍然需要仔细研究技术。例如，“计算机证据可能不像我们想象的那样陌生，” Dedeo说。最近，他与斯坦福大学的计算机科学家Scott Viteri一起对一些著名的规范证明进行了反向工程（包括一些起点）Euclid）和计算机程序生成的数十个证明以证明Coq定理寻找相似之处；他们发现机器证明的分支结构与人造证明的结构非常相似。他说，这种共同性质可以帮助研究人员找到一种方法使辅助程序解释。
“机器证明可能不那么神秘，因为他们似乎，” Dedeo说。
也有人说定理证明是有用的工具，既教计算机科学和数学。在约翰·霍普金斯大学数学家艾米莉·瑞尔开发了一些课程，学生可以使用定理证明者编写证明。她说：“这使他们非常有条理，思路清晰。” “第一次写证明的学生可能不会立即理解他们的要求或掌握逻辑结构。”
Riel还说他最近在工作中越来越多地使用定理证明。她说：“不必一直使用它们，也永远不会取代纸上的涂鸦，但是使用计算机助手作为证据已经改变了我对如何编写证据的理解。”
定理证明者还提供了一种使数学保持公平的方法。 1999年，苏联，俄罗斯和美国数学家弗拉基米尔·亚历山德罗维奇·沃沃斯基（Vladimir Alexandrovich Voevodsky）在他的一份证明中发现了一个错误。从那时起直到2017年去世，他一直积极推动使用计算机来验证证据。 Hales说，他和Ferguson通过使用计算机进行测试，发现了原始证明中的数百种错误。即使是欧几里得基本原理中的第一个定理也不是理想的。如果机器可以帮助数学家避免此类错误，那为什么不利用它呢？哈里斯对此提议提出了实际的反对意见，但是还不知道这样做的合理性：如果数学家不得不花时间对数学进行形式化以使计算机能够理解它，那么他们将无法将时间花在新的数学上。
但是，蒂玛蒂·高尔斯（Timati Gowers），是一位数学家和来自剑桥大学的菲尔兹奖的获得者，他想走的更远：他设想定理证明将在未来的主要期刊中取代人类评论者。“我知道这将如何成为标准做法-如果您希望您的工作被接受，则必须通过自动审阅者来运行它。”
与计算机对话
在计算机可以验证或提供证据之前，研究人员首先需要克服一个重要的障碍：人与计算机的语言之间的沟通障碍。
当今的定理证明者在设计时并未考虑数学家的友好性。第一种类型ATP通常用于测试陈述的真实性，通常通过测试所有可能的选项来进行。询问ATP是否有可能从迈阿密前往西雅图，他可能会穿越从迈阿密通往的所有城市，最后他将找到通往西雅图的城市。
剑桥大学的Timati Gowers认为定理证明将有一天取代人类评论者
使用ATP，程序员可以编写所有规则或公理，然后提出一个问题，即特定的假设是否遵循这些规则。然后计算机完成所有工作。计算机科学家丹尼尔·黄（Daniel Huang）说：“您只需输入要证明的假设，并希望得到答案。”他最近离开加州大学伯克利分校创办了一家初创公司。
但是有一个问题：ATP无法解释其工作。所有计算都在机器内部进行，对于一个人来说，它们看起来像一长串的零和一。 Huang说，不可能查看证明和检验推理，因为它们看起来都像一堆随机数据。他说：“没有人能看到这样的证据并说：一切都清楚。”
第二类，ITP，具有庞大的数据集，其中包含成千上万个定理和证明，通过它们可以检查证明的准确性。与仅在黑匣子中发出答复的ATP不同，ITP需要交互作用，有时还需要人的指导，因此它们并不是那么容易接近。黄说：“一个人可以坐下来，弄清楚正在使用哪些技术来证明。” Dedeo和Viteri研究了此类证据。
近年来，ITP变得越来越流行。在2017年，证明毕达哥拉斯三元组布尔问题的三位一体使用了一个称为Coq的ITP来创建和测试其证明的正式版本。 2005年，微软研究院剑桥的Georges Gontier使用Coq将四色定理形式化。 Hales还使用称为HOL Light和Isabelle的ITP来正式证明开普勒的猜想（HOL代表高阶逻辑）。
今天，该领域的最前沿正在尝试将学习与推理相结合。ATP通常与ITP结合使用以集成机器学习以提高两种技术的性能。专家认为，ATP / ITP程序可以使用演绎推理，甚至可以以与人类相同或至少相似的方式交换数学思想。
推理的局限性
约瑟夫·厄本（Joseph Urban）认为，这种结合的方法可以结合演绎推理和归纳推理，这对于获得证据是必要的。他的小组创建了基于机器学习的定理证明者，使计算机可以自己从经验中学习。在过去的几年中，他们一直在探索神经网络的力量-神经计算单元层，这些层可帮助机器以类似于我们大脑神经元工作方式的方式来处理信息。 7月，他们的小组报告了由经过定理证明训练的神经网络生成的新假设。
在某种程度上，Urban受到了安德烈·卡帕蒂（Andrei Karpaty）的工作的启发，安德烈·卡帕蒂（Andrei Karpaty）几年前训练了一个神经网络，以产生数学上的胡说八道，这似乎使非专业人士信服。但是Urban不需要废话-他和他们的小组开发了自己的工具来搜索证明，并经过数百万个定理的训练。他们使用网络生成新的假设，并使用称为E的ATP程序测试其有效性。
该网络已经发布了50,000多个新公式，尽管已经重复了成千上万的公式。 “看来我们还不能证明更有趣的假设，”厄本说。
Google Research的Szegedi将计算机证据中的自动推理问题视为更广泛领域的一部分：自然语言处理，其中包括识别单词和句子使用的模式。模式识别也是计算机视觉的核心思想，塞格迪此前曾在Google工作过。像其他小组一样，他的团队希望创建定理证明者，以寻找有用的证明并对其进行解释。
受诸如AlphaZero（一种DeepMind的可在国际象棋，围棋和将棋上击败人类的软件）之类的AI工具迅速发展的启发，Szegedi集团希望利用语言识别的最新进展来记录证据。他说语言模型可以证明令人惊讶的准确数学推理。
他在Google Research的小组最近描述了一种使用语言模型（一种神经网络经常使用的语言）来生成新证据的方法。训练模型以识别证明定理的树结构后，他们发起了一项免费实验，只需让神经网络在无监督的情况下生成和证明定理即可。在生成的成千上万个假设中，有13％证明是可证明的且是新的（不重复数据库中的其他定理）。他说，这样的实验表明神经网络在某种意义上可以学习理解证据的模样。
塞格迪说：“神经网络能够发展出一种直觉的人造表面。”
当然，目前尚不清楚这些尝试是否能满足40年前科恩的预言。高尔斯说，他认为到2099年，计算机的推理能力将超过数学家。他说，起初，数学家将享受“黄金时代”，“当他们做有趣的事情而计算机无聊时。但我认为这不会持续很长时间。”
毕竟，如果机器继续发展，并且能够访问大量数据，则它们必须学会做得很好和有趣的事情。高尔斯说：“他们将学会提出自己的要求。”
哈里斯不同意。他认为计算机证明不是必需的，否则计算机证明将最终“使人类数学家变得不必要。”他说，如果计算机科学家能够对合成直觉进行编程，那么它仍然不会与人类直觉竞争。“即使计算机能够理解，他们也不会理解人类。”