第一卷, 第四期
机器的光荣与人的梦想

木 遥

数学文化, 1 (2010), pp. 54-58.

查看节选 查看全文 1813 35966
  • 摘要

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

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