1956年AI研究另外一个重大的突破，是纽厄尔、赫伯特·西蒙等人合作编制的《逻辑理论机》数学定理证明程序（简称LT），从而使机器迈出了逻辑推理的第一步。
在卡内基—梅隆大学的计算机实验室，纽厄尔和西蒙从分析人类解答数学题的技巧入手，让一些人对各种数学题作周密的思考，要求他们不仅写出求解的答案，而且说出自己推理的方法和步骤。通过大量的观察实例，纽厄尔和赫伯特·西蒙广泛收集了人类求解一般性问题的各种方案。他们发现，人们求解数学题通常是用试凑的办法进行的，试凑时不一定列出了所有的可能性，而是用逻辑推理来迅速缩小搜索范围。
经过反复的实验，纽厄尔和赫伯特·西蒙进一步认识到，人类证明数学定理也有类似的思维规律，通过“分解”（把一个复杂问题分解为几个简单的子问题）和“代入”（利用已知常量代入未知的变量）等方法，用已知的定理、公理或解题规则进行试探性推理，直到所有的子问题最终都变成已知的定理或公理，从而解决整个问题。人类求证数学定理也是一种启发式搜索，与电脑下棋的原理异曲同工。
在实验结果的启发下，纽厄尔和赫伯特·西蒙便利用这个LT程序向数学定理发起了激动人心的冲击。电脑果然不孚众望，它一举证明了数学家罗素的数学名著《数学原理》第二章中的38个定理。1963年，经过改进的LT程序在一部更大的电脑上，最终完成了第二章全部52条数学定理的证明。基于这一成功，纽厄尔和赫伯特·西蒙把LT程序扩充到人类求解一般问题的过程，设想用机器模拟具有普遍意义的人类思维活动。他们编制了能解答十种类型不同问题的“通用问题求解程序” （GPS），从而开拓出人工智能中“问题求解”的一大领域。
在纽厄尔和赫伯特·西蒙之后，美籍华人学者、洛克菲勒大学教授王浩在“自动定理证明”上获得了更大的成就。1959年，王浩用他首创的“王氏算法”，在一台速度不高的IBM704电脑上再次向《数学原理》发起挑战。不到9 分钟，王浩的机器把这本数学史上视为里程碑的著作中全部（350条以上） 的定理，统统证明了一遍。该书作者、数学大师罗素得知此事后感慨万端，他在信里写到：“我真希望，在怀海特和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。”王浩教授因此被国际上公认为机器定理证明的开拓者之一。