吴文俊与数学机械化

机器证明的思想可以回溯到17世纪的Descartes与Leibnize,20世纪初Hilbert更明确地提出了公理系统的机械化判定问题，但是，随后的种种努力都未能使机器证明取得本质的进展。近20年来，吴俊继承并发展了中国古代的数学思想，在定理机器证明上开创了以多项式组零点集为基本点的消元方法；吴俊的数学机械化方法已在物理规律的发现，机器人学，计算机视觉以及促进现代数学研究等重大高科技的前沿领域实现了成功的应用。数学机械化研究的兴趣，是中国当代数学发展中一个引人瞩目的具有中国传统特色的新里程碑。

Wu Wen-tsun and Mathematics Mechanization

The idea of proving theorems mechanically may be dated back to Descartes and Leibnize in the 17th century and has been formulated in precise mathematical forms in the 20th 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.