Year: 2010
数学文化, Vol. 1 (2010), Iss. 4 : pp. 54–58
Abstract
仅就解决问题的方式而言，数学是一个由计算与证明组成的学科。计算——无论多么繁琐——本质上都是可以由机械实现的，在今天更是借助电脑的辅助成为一种相对平凡的任务。而证明才被认为是数学本质的困难所在，是人类智慧的高度结晶。那么有没有可能将数学证明也交由机器完成呢？这实在是一个诱人的想法——如果一旦可以实现，那么这将帮助人类完成多少脑力工作！而这是否也意味着数学家这一职业的消失？
在可预见的将来，这些都显得不太现实。那么不妨退一步：利用电脑为人类已有的证明建立可靠的逻辑基础。这听起来似乎不太难以实现，但事实上呢？这条路即便现在看起来依然是那么的迷雾重重、漫长曲折，而我们只不过刚刚起步。为了机器的光荣与人的梦想，我们毅然踏上了征途，结局如何？——证毕。想象一下计算机说出这两个字的感觉……
You do not have full access to this article.
Already a Subscriber? Sign in as an individual or via your institution
Journal Article Details
Publisher Name: Global Science Press
Language: Multiple languages
DOI: https://doi.org/2010-MC-11410
数学文化, Vol. 1 (2010), Iss. 4 : pp. 54–58
Published online: 2010-01
AMS Subject Headings:
Copyright: COPYRIGHT: © Global Science Press
Pages: 5