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/