数学机械化丛书宗旨

十七世纪以来，人类经历了一场史无前例的技术革命，出现了以蒸汽机为代表的机器、代替各种类型的体力劳动。如果说工业机器的出现导致的产业革命使人们逐渐实现了体力劳动的机械化,促进了社会生产力的发展，那么本世纪电子计算机的产生，则为人类实现脑力劳动的机械化创造了物质条件。与工业革命相适应出现了解析几何与微积分这些数学上的伟大创新。在目前这一以计算机为标志的信息革命时代，数学应该有什么样的创新与之相适应呢？正是基于这种考虑，吴文俊先生倡导数学机械化研究。

数学是典型的脑力劳动，因此在脑力劳动机械化过程中有其特殊地位。不仅如此，数学是自然科学与高科技的理论基础，数学方法的创新有可能带动科学发展与技术进步。因而，数学机械化又有其迫切性与优先权。此外，数学具有表达精确、论证严谨等特点，数学机械化在各类脑力劳动的机械化中又易于实现。事实也的确如此。初等几何定理证明被认为是典型的脑力劳动，而吴文俊研究数学机械化正是从这里打开突破口的。

回顾数学发展史，主要有两种思想：一是公理化思想，另一是机械化思想。前者源于希腊，后者则贯穿整个中国古代数学。这两种思想对数学发展都曾起过巨大作用。从汉初完成的《九章算术》中对开平方，开立方的机械化过程的描述到宋元时代发展起来的求解高次代数方程组的机械化方法，无一不与数学机械化思想有关，并对数学的发展起了巨大的作用。公理化思想在现代数学，尤其是纯粹数学中占据着统治地位。然而，检查数学史可以发现数学多次重大跃进无不与机械化思想有关。数学启蒙中的四则运算由于代数学的出现而实现了机械化。线性方程组求解中的消去法是机械化思想的杰作。对近代数学起着决定作用的微积分也是得益于经阿拉伯传入欧洲的东方数学的机械化思想。既便在现代纯粹数学研究中，机械化思想也一直发挥着重大作用。Hilbert倡导的数理逻辑为计算机的设计原理做了准备。数学巨匠E. Cartan关于微分方程、微分几何及李群的著作中经常显现出机械化特色。H. Cartan关于代数拓扑学同调群计算的工作可以看作是机械化思想的成功范例。

数学机械化主要有两个步骤。一是算法化。数学的机械化有赖于计算机的使用。数学要实现机械化就必须适当地变革自己以适应计算机有限性、离散性，特别是算法性的特点。二是机械化，既在计算机上有效地实现有关算法。在这一步有效性是至关重要地，只有有效的软件才能真正用来解决实际问题。以机械化数学为基础的软件可以实现人力难以胜任的繁琐的计算与推理功能，从而为数学研究提供新工具、为数学在高科技中的应用提供有力手段。

数学机械化的目标是在数学的各个分支实现机械化。当然，由Gödel以及其他的关于判定问题的否定性结果，我们知道很多数学领域是不能机械化的。吴文俊设想，数学的机械化过程应该是选择一些既有意义又可以有效算法化的问题类，加以解决，变传统的一题一证为一类一证。

七十年代，吴文俊由中国传统数学中的机械化思想出发，从几何定理证明入手开始数学机械化研究，所建立的数学机械化方法，为国际自动推理的研究开辟了新的前景。经过近二十年的努力，几何定理自动证明的吴方法及在其影响下产生的一系列重要的新方法，已经发展成具有我国特色且在国际上领先的数学机械化理论，形成了自动推理与方程求解的中国学派。数学机械化理论不仅在微分几何、理论物理、力学等领域得到成功应用，还为机器人学、数控技术、几何辅助设计、CAD、计算机视觉等高科技领域提供了有力工具。

该丛书的宗旨是对近二十年来我国学者在数学机械化领域的研究成果给予系统的介绍，以推动数学机械化研究的发展，并希望对数学机械化理论与方法的应用提供方便。