数学自动定理证明的前景

Argonne National LaboratoryCPU产品的正确性。数学家的奇思妙想终于有了实际用场。

如今，在通用计算机上搞数学定理的”自动证明“已经不是难事，自由软件与商品软件很多，可谓”一抓一大把“。但是，机器自动定理证明的前景如何呢？

我们这一代人已经老了，没有什么用处了。我想，我的小孙孙这一代，从小就在计算机上”泡“，长大了之后，习惯于找计算机“医生”看病（人工智能专家系统）；学习数学时，满脑袋里面不再是某某数学家证明了什么定理，而是某某计算机程序”证明‘了什么什么定理。在他们看来，数学就是计算机搞出来的”学问“。

我认为，数学不是计算机下的”蛋“，而是人脑的”分泌物“。从本质上讲，数学是数学家做的事情，离开了人，谈何数学？

袁萌日

人之所以能，是相信能。