数学形式化的现代意义            

十八世纪下半叶，使用形式语言工具研究数学自身的规律，引发当代数学的兴起。1911-13年，罗素《数学原理》的发布，将基础数学全部形式化，在数学界，这是一重大事件。

上世纪60年代，我国大搞文革运动，视形式化为“形而上学”，错过了发展机会。在此期间，基于形式化方法的“自动推理”（AR，Automated Reasoning）算法在国外蓬勃发展起来（注：AR属于人工智能AI研究领域）。直到上世纪90年代，各种AR软件相继涌现。事实证明，与《数学原理》相比，在一定条件下，机器证明的技巧要比人类高明，机器证明的步骤比人类要少一些.

至此，这些AR软件成为人类数学证明的好帮手，也是集成电路设计的必必需工具。

如今，我们建设强大国家，离开形式化数学，是绝对不行的。

  说明：形式化、公理化是当代数学发展的主线。偏离了发展主线一定会掉进小水沟。

袁萌   10月30日