在已有工作的基础上，本文从总体的和全面的角度着眼，从数学机械化思想发展的关键人物和关键事件入手，结合对重点案例的分析，综合考察了数学机械化思想发展的历史过程，特别是揭示数学机械化思想的产生和发展。 已有研究工作对数学机械化的思想发展虽有认识，但系统、全面地揭示其发展脉络仍是数学史研究地重要课题。本文从笛卡尔、莱布尼茨关于机械代替人脑处理数学设想出发，进一步揭示了希尔伯特的数学机械化方法，塔斯基、王浩的创造性工作，以及吴文俊的卓越贡献，为更深刻地理解数学机械化思想提供了有力的支撑。 国内的数学机械化研究一直关注吴文俊院士的已有成果，对西方学者的研究方法和思路介绍不多。本文在研读西方文献的基础上，比较详细地介绍了数学机械化研究在西方的发展，特别突出了西方学者对于数学机械化的不同理解和研究取向。 本文的重点在于介绍塔斯基和王浩在数学机械化研究中的贡献。塔斯基首先在理论上证明：初等几何和代数范围的命题都可以通过机械方法判定。塔斯基得出的结论给定理判定问题的研究带来了曙光，虽然哥德尔不完备定理否定了希尔伯特的思路，但是在其它方向寻找判定方法是可行的。 电子计算机的诞生为数学机械化做好了物质条件上的准备。1959年，华裔逻辑学家王浩在IBM 704型计算机上编制的程序高效地证明了《数学原理》中的220条定理，正是王浩吹响了向数学机械化迈进的号角。王浩强调算法的重要性，合理的算法可以最大限度的发挥使计算机的效力。王浩提出，计算与证明存在不同之处，将证明转化为计算是实现数学问题机器证明的根本途径；应当注意通常的多项式复杂类，并认为这是有可能取得突破的方向。 王浩的思想无疑是正确的。吴文俊数学机械化方法的成功正是由于找到了处理多项式复杂关系的有力工具。更为可喜的是，吴文俊的数学机械化方法是在不了解西方学者研究的情况下独立取得的，而促成这一突破性成果的主要思想竟然来自中国古代的数学家。蕴含于中国传统数学中的方程解法和算法化思想在数学机械化的研究中大放异彩，揭示了具有机械化特征的中国传统数学思想的强大生命力。 数学机械化的思想源自西方，但是高效、广泛的定理机械化证明方法的得出，却得益于具有机械化特征的中国传统数学思想的启发。对数学机械化思想发展的历史研究充分说明，中国传统数学思想对于数学发展有其独特贡献，机械化的数学与电子计算机的紧密结合，必将深刻改变人们研究数学的方式，必将从根本上影响数学的发展。 本文在附录中给出了C语言描述的“增乘开放法”，以及运用数学机械化自动推理平台( MMP )实现定理证明的实例。 通过对数学机械化思想的历史回溯，本文还提出了有待进一步探讨的问题。