计算机自动化数学推理的距离有多近？
在1970年代，已故的数学家保罗·科恩（Paul Cohen）是唯一赢得数学逻辑工作的领域奖牌的人，据说做出了一个详尽的预测，继续激发和刺激数学家 - “在某些未指定的未来时间，数学家将被计算机取代。”科恩（Cohen）是他在统计理论中的大胆方法的传奇人物，他预测所有数学都可以自动化，包括撰写证明。
证明是一个逐步的逻辑论点，可以验证一个事实推测，或数学命题。（一旦证明，猜想就变成了一个定理。）它都建立了陈述的有效性，并解释了为什么它是正确的。不过，证明很奇怪。这是抽象的，并且不受重大体验的束缚。认知科学家说：“它们是一个虚构的，非物理世界和生物学发展的生物之间的疯狂接触。”西蒙·德德（Simon Dedeo）卡内基·梅隆大学（Carnegie Mellon University），他通过分析证明结构来研究数学确定性。“我们没有进化。”
计算机对于大计算很有用，但是证明需要不同的东西。猜想是由归纳推理引起的 - 一种关于一个有趣问题的直觉 - 通常遵循演绎，逐步逻辑。他们通常需要复杂的创意思维，以及填补空白的更费力的工作，机器无法实现这种组合。
计算机化定理抛弃可以分为两类。自动化定理掠夺者或ATPS通常使用蛮力方法通过大计算来处理。交互式定理抛弃或iTP充当证明助手，可以验证论点的准确性并检查现有证明是否错误。但是，即使合并了这两种策略（与较新的定理掠夺一样），也不会加起来自动推理。
另外，这些工具尚未张开双臂，大多数数学家都不使用或欢迎它们。Dedeo说：“对于数学家来说，他们非常有争议。”“他们中的大多数不喜欢这个主意。”
该领域的一个巨大的开放挑战询问实际可以自动化多少证明：系统可以产生有趣的猜想并以人们理解的方式证明这一点吗？世界各地实验室的最新进展提出了人工智能工具可以回答该问题的方法。布拉格捷克信息学，机器人技术和控制论研究所的约瑟夫城市正在探索各种方法，这些方法使用机器学习来提高现有掠夺者的效率和性能。七月，他的团队报告一组原始的猜想和证明是由机器生成和验证的。6月，Google Research的一个小组领导基督教Szegedy从努力来利用自然语言处理的优势来使计算机证明在结构和解释方面更具人性化。
一些数学家将定理掠夺视为一种可能改变游戏规则的工具，用于培训证明写作的本科生。其他人则说，让计算机编写证明是不必要的，这对于推进数学而言可能是不可能的。但是，一个可以预测有用的猜想并证明新定理的系统将实现新的目标 - 某些机器版本的理解版本。这表明有可能自动理性本身。