１９５６年，美国卡内基大学—兰德公司协作组在电子计算机上成功地证明了罗素和怀特海所著的《数学原理》第二章５２条定理中的３８条。这是机器证明的开始。
１９５９年，美籍华人王浩教授只用９分钟的机器时间，就在计算机上证明了罗素和怀特海《数学原理》一书中的一阶逻辑部分的全部定理３５０多条，引起数学界的轰动。机器证明是用电子计算机来完成数学命题的证明，它是现代数学中一种新兴的边缘性学科，是现代人工智能发展的一个重要方向。改进算法程序是提高机器证明效率的重要方面，１９６５年美国数学家鲁滨逊提出了著名的归结原理，该原理的基本出发点是，要证明任何一个命题为真，都可以通过证明其否定为假来得到。１９７６年，美国数学家阿佩尔和黑肯借助于计算机，成功地证明了“四色猜想”，这是机器证明首次解决传统人脑支配的手工证明所没有解决的重要难题。１９７１～１９７７年间，莱德索等人给出了分析拓扑学和集合论方面的一些著名定理的机器证明。１９７９年，波依尔和穆尔等人作出了递归函数方面的机器证明系统。１９７７年，中国数学家吴文俊证明了初等几何一类主 要定理的证明可以机械化；１９８０年，他还用一部微机在２０和６０个机器小时左右分别发现了两个几何学的新定理，这些成果引起了学术界的关注。从传统的手工证明到定理的机器证明，是现代数学思想方法的一次重大飞跃。
