吴文俊与数学机械化..docVIP

吴文俊与数学机械化 纪志刚 上海交通大学学报，2001 年第3 期 摘 要 ：机器证明的思想可以回溯到 17 世纪的 Descartes 与 Leibnize ， 20 世纪初 Hilbert 更明确地提出了公理系统的机械化判定问题。但是，随后的种种努力都未能使机器证明取得本质的进展。 近 20 年来，吴文俊继承并发展了中国古代的数学思想，在定理机器证明上开创了以多项式组零点集为基本点的消元方法；吴文俊的数学机械化方法已在物理规律的发现、机器人学、计算机视觉以及促进现代数学研究等重大高科技的前沿领域实现了成功的应用。数学机械化研究的兴起，是中国当代数学发展中一个引人瞩目的具有中国传统特色的新里程碑。 关键词 ：机器证明；数学机械化；中国古代数学； 中图分类号： 文献标识码： 文章编号 ： Wu Wen-tsun and Mathematics Mechanization JI Zhi-gang (Department for the History of Science Philosophy of Science,Shanghai Jiao Tong University , Shanghai 200030, China) Abstract: The idea of proving theorems mechanically may be dated back to Descartes and Leibnize in the 17 th Century and has been formulated in precise mathematical forms in the 20 th century through the school of Hilbert. In spite of vigorous efforts, however, researches in this direction give rise quite often to negative results. For example, the methods of Tarski based on a generalization of Sturm are still too complicated to be feasible, even with the use of computers. It is Wu Wen-tsun who established a new algorithm for the mechanization of theorem-proving in elementary geometry. Wu’s methods were all originated and quite developed from ancient Chinese mathematics. In fact, the algebrization of geometrical problems and systematic method of their solution by algebraic tools were some of the main achievements of classical Chinese mathematics. Now, the method of mathematical mechanization has been played an important role in mathematics, and gotten its wide applications. Key words: mechanical proving ； mathematics mechanization ； classical Chinese mathematics ； Wu Wen-tsun 一、机器证明：古老的梦想 相传 Ptolemy 王曾向 Euclid 请教学习几何的捷径， Euclid 没有屈从帝王的尊严，直率地说：几何中无王者之路 ( There is no royal way in geometry ) 。 以希腊的几何学为代表的古代西方数学，其特点是在构造公理体系的基础上证明各式各样的几何命题。几何题的证法，各具巧思，争奇斗艳，无定法可循，只有依赖个人的经验、技巧和灵感。 学习几何的孩子做梦都在想：要是几何题象解一元二次方程那样多好。这种愿望由来已久， 17 世纪法国的数学家 Descartes 曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。” Descartes 把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方