几何定理的机器证明——每个中国数学教师都应懂得的方法

Mechanical Theorem Proving in Geometry

本文着重介绍了几何定理的机器证明的开拓者和奠基人——吴文俊院士创立的“吴法”及其主要成员张景中院士的“消标点法”和杨路教授的“降维算法”。

In this paper, we present three kind of computerized methods for geometrical theorem proving, the first is Prof. Wu Wenjun who introduced the method of equations solving, i. e., the polynomials system solving, known as Wu' s method in the international community, Wu' s method makes the highly effective automatic proving of the geometrical theorems possible for the first time, and his contribution leads the Chinese mathematics into the top position in this field of the world, the second is Prof. Zhang jingzhong, known ad Elimination Point Method. And the third is Prof. Yang lu, known as lower Dimension Method.