计算机辅助证明

计算机辅助证明是一种部分或全部内容以电脑协助之数学证明。

哲学争议

编辑

由于大部分的计算机辅助证明计算量庞大,无法以人手验证,很多数学家[谁?]不接受计算机辅助证明,并表示那只是计算而非证明。他们[谁?]表示,美丽的数学证明应像首诗,而电脑证明则看似电话簿。

历史

编辑

第一个著名的计算机辅助证明,是1976年的四色定理证明。

著名的计算机辅助证明

编辑

参考

编辑

外部链接

编辑