7月2日下午，北京市小学开始放暑假，二楼的小孙孙不停地大喊大叫，对此，我心中很烦。但是，上楼一看，发现小孙孙正在网络上与同学玩连网游戏，...引起我对往事的回忆。

     上世纪50年代，通用计算机刚刚问世（1954年），数学家就在计算机上动脑筋了，想搞“机器自动定理证明”。起初，他们（数学家）拿罗素名著“数学原理”开刀（小试牛刀），在三条推理规则（模块生成、变量代换与公式置换）的前提下，让计算机自动证明了“数学原理“中前54个定理的38个，可谓”旗开得胜“也。

    从1960年开始，美国国家实验室（Argonne National Laboratory）投入大量人力研究”自动定理证明“技术，后来，英特尔、AMD使用这种”自动化“技术验证CPU产品的正确性。数学家的奇思妙想终于有了实际用场。

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

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

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

袁萌 7月3日