据报道，在1970年代，已故的数学家保罗·科恩（Paul Cohen）是唯一获得过数学逻辑领域勋章的人，据此做出了一个广泛的预测，这一预测继续激起和激发了数学家——“在未来的某个不确定的时期，计算机将取代数学家。”因在集合论中大胆的方法而闻名的科恩（Cohen）预测，所有数学都是可以自动化的，包括编写证明。
证明是一步一步的逻辑论证，它验证猜想或数学命题的真实性。（一旦证明，猜想就成为一个定理。）它既可以建立陈述的有效性，又可以解释其成立的原因。但是，证明很奇怪。它是抽象的，不受物质体验的束缚。卡内基梅隆大学的认知科学家西蒙·德迪奥（Simon DeDeo）说：“这是假想的非物质世界与生物进化的生物之间的疯狂接触。”他通过分析证明的结构来研究数学确定性。“我们并没有这样做。”
计算机对于大型计算很有用，但证明要求有所不同。归纳推理是一种关于一个有趣问题的直觉，它来自于归纳推理，而证明通常遵循推论，逐步的逻辑。它们通常需要复杂的创造性思维以及需要付出更多努力才能填补空白，而机器无法实现这种结合。
计算机定理证明者可以分为两类。自动化定理证明者（ATP）通常使用蛮力方法进行大量计算。交互式定理证明者（ITP）充当证明助手，可以验证参数的准确性并检查现有证明是否有错误。但是，即使结合使用这两种策略（如较新的定理证明就是这种情况），它们也不会合计为自动推理。
另外，这些工具还没有被推广或被广泛认可，大多数数学家也不使用或欢迎它们。“对于数学家来说，这是非常有争议的。”德迪奥说，“大多数人不喜欢这个主意。”
这个领域的一个艰巨的开放挑战会问，实际上有多少校样可以自动化：一个系统能产生一个有趣的猜想，并用人们理解的方式来证明它吗？来自世界各地实验室的一系列最新进展表明，人工智能工具可以回答这个问题。布拉格捷克信息学、机器人学和网络学研究所的约瑟夫·厄本（Josef Urban），正在探索各种使用机器学习来提高现有证明者效率和性能的方法。7月，他的小组报告了一组由机器生成和验证的原始推测和证据。今年6月，由克里斯蒂安·塞格迪（Christian Szegedy）领导的谷歌（Google）研究公司小组发布了最新成果，这些成果是利用自然语言处理的优势，使计算机证明在结构和解释上更加人性化的结果。
一些数学家认为定理证明是潜在的改变游戏规则的工具，可以训练大学生进行证明写作。其他人则说，让计算机编写证明对于推进数学是不必要的，而且可能是不可能的。但是，一个可以预测有用猜想并证明新定理的系统将会实现一些新的东西——某种机器版本的理解，塞格迪说，这就暗示了自动实现推理本身的可能性。有用的机器
长期以来，数学家、逻辑学家和哲学家一直在争论证明的哪一部分是人为因素，如今有关机械化数学的争论仍在继续，尤其是在连接计算机科学和纯数学的深谷中。
对于计算机科学家来说，定理证明没有争议。它们提供了一种严格的方法来验证程序是否有效，关于直觉和创造力的争论不如找到解决问题的有效方法重要。例如，在麻省理工学院，计算机科学家亚当·克莱帕拉（Adam Chlipala）设计了定理证明工具，该工具生成传统上由人类编写的加密算法，以保护互联网交易。他小组的代码已经用于Google Chrome浏览器上的大多数通信。
克莱帕拉说：“您可以采用任何一种数学参数，并使用一个工具对其进行编码，然后将您的参数连接在一起以创建安全性证明。”
在数学中，定理证明者帮助产生了复杂的，计算繁重的证明，否则这些证明将占用数以百计的数学家的生命。开普勒猜想描述了堆叠球体（或从历史上说是橘子或炮弹）的最佳方法，它提供了一个很好的例子。 1998年，托马斯·海尔斯（Thomas Hales）和他的学生山姆·弗格森（Sam Ferguson）一起使用各种计算机数学技术完成了证明。结果是如此繁琐（结果占用了3 GB），以至于12位数学家对它进行了长达数年的分析，然后才宣布99％的观点是正确的。
开普勒猜想并不是机器可以解决的唯一著名问题。四色定理说，您只需要用四种颜色就可以对任何二维图进行着色，这样就不会有两个相邻的区域共享一种颜色。数学家于1977年使用计算机程序对四色定理进行了定理，该程序通过五色图进行显示。都可以减少到四个。在2016年，三位数学家使用计算机程序来证明长期存在的公开挑战（称为布尔毕达哥拉斯三元组问题），但该证明的初始版本为200 TB。有了高速互联网连接，如果你要下载它需要三周多的时间。复杂的感觉
这些例子通常被称为成功，但它们也增加了争论。证明四色定理的计算机代码已经有40多年的历史了，人类无法自行检查。哥伦比亚大学的数学家迈克尔·哈里斯（Michael Harris）说：“从那以后，数学家们一直在争论，这是否是一个证明。”
另一个困扰是，如果他们想使用定理证明，数学家必须首先学习编码，然后弄清楚如何用计算机友好的语言表达他们的问题，这是不利于进行数学运算的活动。哈里斯说：“当我将问题重新组织成适合该技术的形式时，我自己就会解决问题。”
许多人只是认为他们的工作中不需要定理求解器。伦敦帝国理工学院的数学家凯文·巴扎德（Kevin Buzzard）说：“它们有一个系统，它可以用铅笔和纸书写，并且可以工作。”三年前，他将工作从纯粹的数学转向了定理证明和形式证明。“计算机为我们做了惊人的计算，但它们从来没有独自解决难题。”他说，“直到他们这样做，数学家们才不会购买这种东西。”
但是巴扎德和其他人认为也许他们应该这样做。一方面，“计算机证明可能不像我们想象的那样陌生，” 德迪奥说。最近，他与现在斯坦福大学的计算机科学家斯科特·维特里（Scott Viteri）进行了逆向工程，对少数著名的经典证明（包括Euclid's Elements的其中之一）和数十个使用定理证明器Coq编写的机器生成的证明进行了查找。为了共同点。他们发现，机器证明的网络结构与人们制作的证明的结构非常相似。他说，这种共有的特征可能会帮助研究人员找到一种方法，从某种意义上说来证明自己的助手。
德迪奥说：“机器证据可能并不像看起来那样神秘。”
还有人说，定理证明者可以是计算机科学和数学领域中有用的教学工具。在约翰霍普金斯大学，数学家艾米丽·里尔（Emily Riehl）开发了一些课程，学生可以使用定理证明者来编写证明。“这迫使您组织得井井有条，思路清晰。”她说，“第一次写证明的学生可能很难知道他们需要什么并理解逻辑结构。”
里尔还说，她在自己的工作中越来越多地使用定理证明。她说：“不一定要一直使用它，也永远不能代替在纸上划划写写，但是使用校对助手已经改变了我思考编写校样的方式。”
定理证明者还提供了一种保持领域诚实的方法。1999年，俄裔美国数学家弗拉基米尔·沃沃斯基（Vladimir Voevodsky）在他的证明中发现了一个错误。从那时起直到2017年去世，他一直是使用计算机检查证明的拥护者。海尔斯说，他和弗格森在用计算机检查原始证明时发现了数百个错误。即使是《欧几里得的元素》中的第一个命题也不是完美的。如果机器可以帮助数学家避免此类错误，那为什么不利用它呢？ （海尔斯提出的反对意见是有道理的还是没有道理的：如果数学家们不得不花时间将数学形式化以被计算机理解，那么他们就不必花时间去做新的数学了。）
但是，剑桥大学的数学家和菲尔兹奖得主蒂莫西·高尔斯（Timothy Gowers）希望走得更远：他设想了一个定理证明将取代主要期刊上的人类裁判的未来。他说：“我可以看到，如果您希望您的论文被接受，则必须通过自动检查器，这已成为一种标准做法。”与计算机交谈
但是在计算机可以普遍检查甚至设计证据之前，研究人员首先必须扫除一个重要的障碍：人类语言与计算机的语言之间的沟通障碍。
当今的定理证明并不是为了方便数学家而设计的。第一种类型的ATP通常用于检验陈述是否正确（通常通过测试可能的情况）。例如，要求ATP验证一个人可以从迈阿密开车到西雅图，并且它可能会搜索所有从迈阿密出发的道路所连接的城市，并最终找到一条通往西雅图的道路。
使用ATP，程序员可以编写所有规则或公理的代码，然后询问是否有一个特定的猜想遵循这些规则。然后，计算机完成所有工作。计算机科学家丹尼尔·黄（Daniel Huang）说：“您只要输入要证明的猜想，就可以希望得到答案。”他最近离开加州大学伯克利分校，在一家创业公司工作。
但是有一个难题：ATP不做的就是解释其工作。所有这些计算都发生在机器内部，在人眼看来，它就像一串长长的0和1。黄说，因为看起来像一堆随机数据，所以不可能扫描证明并遵循推理。他说：“没有人会看那个证据，并且会说'我明白了'。”
ITP是第二类，具有庞大的数据集，其中包含多达数万个定理和证明，他们可以对其进行扫描以验证证明是正确的。与仅在黑匣子中工作并吐出答案的ATP不同，ITP在过程中需要人与人之间的互动甚至是指导，因此它们并非难以获得。黄说：“人们可以坐下来，了解什么是证明级技术。”
近年来，ITP变得越来越流行。2017年，布尔毕达哥拉斯三元组问题背后的三重奏使用了ITP Coq，来创建和验证其证明的正式版本；在2005年，微软研究院（剑桥）的乔治·贡蒂埃（Georges Gonthier）使用Coq将四色定理形式化。哈里斯在开普勒猜想的正式证明中还使用了称为HOL Light和Isabelle的ITP。 （“ HOL”代表“高阶逻辑”。）
今天，在该领域最前沿的努力旨在将学习与推理相结合。他们经常将ATP与ITP结合在一起，并且还集成了机器学习工具来提高两者的效率。他们设想可以使用演绎推理（甚至可以传达数学思想）的ATP / ITP程序，其方式与人们的做法相同，或者至少以类似的方式。理性的极限
约瑟夫·厄本（Josef Urban）认为，证明所需的演绎推理和归纳推理的结合可以通过这种组合方法来实现。他的小组建立了以机器学习工具为指导的定理证明者，使计算机可以通过经验自己学习。在过去的几年中，他们探索了神经网络的使用——神经计算的各个层，它们通过大致模拟我们大脑的神经元活动来帮助机器处理信息。7月，他的小组报告了由经过定理证明数据训练的神经网络产生的新猜想。
厄本受到安德烈·卡尔帕西（Andrej Karpathy）的部分启发，安德烈·卡帕西（Andrej Karpathy）几年前训练了一个神经网络，以生成看起来像数学的谬论，这对非专家而言是合法的。不过，厄本不想要废话，而是他和他的团队设计了自己的工具，在经过数百万个定理的训练后，可以找到新的证明。然后他们使用网络生成新的猜想，并使用称为E的ATP检查了这些猜想的有效性。
该网络提出了50,000多个新公式，尽管有数千个重复。乌尔班说：“看来我们还没有能力证明更有趣的猜想。”
谷歌研究公司的塞格迪将计算机证明中的自动推理视为更大领域的一个子集：自然语言处理，这涉及在单词和句子的使用中进行模式识别。（模式识别也是计算机视觉背后的驱动思想，这是塞格迪之前在谷歌的项目的目标。）与其他小组一样，他的团队也希望定理证明者能够找到并解释有用的证明。
受诸如AlphaZero（可以在国际象棋，围棋和将棋上击败人类的DeepMind程序）之类的AI工具迅速发展的启发，塞格迪的小组希望利用语言识别的最新进展来编写证明。他说，语言模型可以证明令人惊讶的扎实的数学推理。
他在谷歌研究公司的小组最近描述了一种使用语言模型（通常使用神经网络）生成新证据的方法。训练模型以识别已知定理中的某种树状结构后，他们进行了一种自由形式的实验，只需要求网络生成并证明一个定理，而无需任何进一步的指导。在成千上万的猜想中，约有13％都是可证明的和新的（这意味着它们没有重复数据库中的其他定理）。他说，该实验表明，神经网络可以自学一种对证明看起来像什么的理解。
塞格迪说：“神经网络能够发展出一种人工的直觉风格。”
当然，目前还不清楚这些努力是否能满足40年前科恩的预言。高尔斯曾表示，他认为到2099年，计算机将能够超越数学家但我认为这将持续很短的时间。”
毕竟，如果机器继续改进，并且可以访问大量数据，那么它们也应该变得非常擅长于完成有趣的部分。 高尔斯说：“他们将学习如何做自己的提示。”
哈里斯不同意。他认为计算机专家不是必需的，否则他们将不可避免地“使人类数学家过时”。 他说，如果计算机科学家能够对一种合成的直觉进行编程，那么它仍然无法与人类相提并论。“即使计算机能够理解，它们也无法以人类的方式理解。”
