不好意思，回晚了，是这样的。 [ 厚积薄发 ] 于:2007-12-11 20:59:26
我当时的设想是找到一套公理系统，所有关于定理证明的形式逻辑都可以用相应的符号表示，对于每个定理的证明就变成纯粹地变动符号了。哲学在这个体系下的位置就是类似于某种普适的原则，用于发现新定理和相应的证明。

打个比喻，就好比我有三万的英语词汇量，而且对英语的语法烂熟于胸。那末写作对于我来讲就是纯粹地对词汇根据相应的语法规则进行排列组合。理论上我也是可以写出《哈姆莱特》的。

我所说的“我总是不停地发现那些漂亮的证明们常常来自于我已经努力构造好的哲学圈子之外”，就类似于莎士比亚写《哈姆莱特》并不是在机械地玩文字的排列组合一样，是他的思想驱动文字。发现证明有两方面。一方面是在现有的概念框架下进行证明。在证明完成的时候，看起来好像就真的是一系列逻辑的组合，让人产生一种“证明也可以机械化”的感觉。这也是我大学一年级才开始学习数学分析时想要做的。这个想法的关键困难在于你如何巧妙地对概念进行合理的逻辑组合，从而得到你想要的结果。在当时这已经超过了我的能力，所以失败也不足为奇了。后来我才领悟到，对于数学分析的学习来说，指引我们找到证明的往往是几何直观--画一个图，看看函数为什么会有定理中所说的性质，然后把这些性质转化成严格的逻辑语言。一个最简单的例子就是证明如果一个连续函数在0点取值x，在1点取值y，那末这个函数在0和1之间可以取到所有在x和y之间的值。画个图，这是显而易见的，可是要严格说清楚，就要用到紧集的概念--即当我们不断用二分的方法来找某个介于x和y之间的取值时，我们要确保一系列的区间最后能交于一点。[0,1]就是紧集。

发现证明的另一方面来自于不断地引入新概念。数学的研究，说创造也好，说发现也好，有一个不断研究新问题的过程。在研究过程中会需要引入新概念，例如在研究费尔马大定理的过程中发现要研究新的数域。十九世纪试图解决费尔马大定理的努力在很大程度上是现代数论的开端，所以高斯说费尔马大定理是一个下金蛋的母鸡。

说说我当时为什么会产生这种“把证明给机械化”的念头。当时学习微积分，一上来讲的就是用义普斯隆-德尔塔语言把极限的概念给严格化。这种抽象化使得我产生了一种错觉，“数学就是这样创造出来的，就是这样抽象而严密的。”实际上不是这样的。极限概念的严格化是微积分发明后两百年才发生的。一开始，大家都忙着用微积分解决各种各样的问题，尤其是和物理有关的问题。所以有一百多年的时间，微积分并没有严格的逻辑基础，但是大家却依赖于直观在“正确”地使用它，这一百多年的时间被称为“微积分的英雄时代”，因为大量重要的实际问题被微积分给解决掉了。直到随着微积分使用的越来越深入，人们发现有些基本的概念必须从逻辑上讲清楚，才回过头来解决这些问题。

我当时犯错误在于一没有把数学放入到历史发展的语境下来理解，误认为数学就是这样严密而抽象的；二在于从小都是在不好的学校上学，没有真正地学会如何解题，缺乏实际理解并解决问题的能力和经验。（所以搞搞课外兴趣小组，竞赛培训还是可以的，目的在于启蒙。）

我博士毕业后在学校教书的时候，也有学生产生类似的想法，所以在对科学的体会中，并不是我一个人会走上歧途。这也说明科学传承的重要性--名师出高徒就在于老师可以把学生很快的领进门，避免走弯路，同时把最宝贵的经验传授给学生。

关于机械证明，也有人在研究，国内是吴文俊教授。当然他们做的可是比我原始粗糙的想法高级精细多了。

时间太晚，就不多说了。最后讲讲自己的一些触类旁通吧。我前面提到的两个犯错原因中，如果把学习数学变成建设现代国家的话，可以帮助我理解中国现在的很多问题所在。所以我强调要读历史，尤其是西方国家在发展现代文明上的宝贵经验。用格林斯潘在他的自传里的话说，"The more we look back, the further we see forward."另外我的教训也说明生搬硬套是没法解决真正有挑战性的问题的，已有的方法只是对适合的对象才有用。河里有懂数据挖掘的人的话，应该听说过这样一句话，“If you torture data sufficiently, it will confess anything.”所以对哲学有一些朴素的感性认识，可以帮助我们判断什么时候可以用数据挖掘，什么时候不能用。这种朴素的辩证法对于科学研究的帮助，以后有机会再专门发帖谈吧。不过我自认为五年之内，我的积累不足以发一个够分量的帖子。

对数学历史有兴趣的河友可以读读《布尔巴基的兴衰》这本小书。这段历史对于说明数学的抽象化的利弊很有用。我读布尔巴基的《拓扑学》和后来实际使用拓扑学，对此比较有感触。

最后于2007-12-11 21:10:06改,共3次;