首先，我不得不歌颂下伟大的数学家们（包含哲学家、逻辑学家们）的智慧，他们兼具洞察力与创造力。
嘛，有时候我觉得数学有点像分类学，数学基础大厦是不可能改变的，只是数学家们从不同角度重新对知识梳理一遍后，让我们又从新的角度去理解了一遍数学，这往往是令人兴奋的。
在对证明还没有任何概念的时候，我学习了数分，之后便想抱起人们常说的很难的课程《实分析》看，现在看来，会觉得「难」是显然的，当然实分析也不仅仅是证明部分难，也涉及到对实数域上很多性质的理解。但真正理解什么是「证明」绝对是十分重要、有帮助的，这意味着对基础概念有了很多基础性知识和扩展性知识的了解和意识。这方面来说，要看懂《抽象代数》也是一样的，或者说，如果不懂「证明」，我更认为先看《抽代》反而更合适（相对于学《实分析》），至少有可能能让你开始意识到某种形式的重要性，或者某种思维方式的重要性，而如果对这块感兴趣，就可以更深入的去学习集合论、数理逻辑的内容。
虽然这么说，然而，我却是在用了一些定理证明助手（Coq/Agda）后，才真正开始有了「证明」的意识，所以，我想说数学家们的脑袋实在太过于聪明。
「证明」在学《实分析》以前的数学体现确实不算是非常明显（包括《数分》，当然不排除有的人已经掌握了这种思维习惯），以至于大部分人（以及我）在学到这个位置时仅仅学会了计算和记忆概念（我想或许是这样，也可能只有我是这样），但回忆起来，高中数学的一些题已经多次强调和在训练我们对「证明」的意识，比如数列、不等式等等。。。但还是对其概念模模糊糊。那时候啊，我觉得什么归纳法、反证法看起来就像废话一样（捂脸），不理解这种证明的意义是啥，没感觉像是证明，更喜欢计算题，算就完事了。多次错过了意识到它的技术原理的魅力，不过呢，好巧不巧，后来是计算机科学 -> 数理逻辑让我入了证明的门，重新开始对这些东西有了新的理解。
集合论、证明论、模型论、递归论等等数理逻辑的内容过于庞大，虽然有一些交叉知识，但一两句话依然是讲不完的，从罗素悖论到公理化系统建立，从 ZF 到 ZFC，从希尔伯特计划到哥德尔的断言，从丘奇、图灵等人对计算的描述到整个计算机科学的发展，从形式主义到构建/直觉主义，从证明到程序，从 Typed lambda calculus 到证明系统，从20世纪到现在，那个时代还没有编程语言，准确的说是编程语言的产物（lambda calculus就是一个最小化计算语言，而产物指现在我们用的编程语言工具），数学家、逻辑学家们仅凭借思考、智慧发现了这些东西，让我实在是佩服得不行。
再次，我不得不歌颂下伟大的数学家们的智慧，潜藏在他们思维中那令人惊叹的洞察力与创造力，蕴含着某种深邃的思想。