仅就解决问题的方式而言，数学是一个由计算与证明组成的学科。计算——无论多么繁琐——本质上都是可以由机械实现的，在今天更是借助电脑的辅助成为一种相对平凡的任务。而证明才被认为是数学本质的困难所在，是人类智慧的高度结晶。那么有没有可能将数学证明也交由机器完成呢？这实在是一个诱人的想法——如果一旦可以实现，那么这将帮助人类完成多少脑力工作！而这是否也意味着数学家这一职业的消失？

在可预见的将来，这些都显得不太现实。那么不妨退一步：利用电脑为人类已有的证明建立可靠的逻辑基础。这听起来似乎不太难以实现，但事实上呢？这条路即便现在看起来依然是那么的迷雾重重、漫长曲折，而我们只不过刚刚起步。为了机器的光荣与人的梦想，我们毅然踏上了征途，结局如何？——证毕。想象一下计算机说出这两个字的感觉……