Geometry Theorem-Proving and Geometry Problem-Solving, Old and New

Wu Wen-tsün (Institute of Systems Science, Academia Sinica)

Abstract

The geometry theorem-proving in ancient Greece is well-known. As for in ancient China, one considered usually geometry problem-solving rather than geometry theorem-proving, and for the latter the theorems to be proved were usually in the form of formulae. Furthermore, instead of set of axioms, the ancient Chinese formulated rather some simple and plausible principles and then proved the formulae or solved the problems by logical reasoning.

A turning point occurred in Song Dynasty (+960, +1274) and Yuan Dynasty (+1271, +1368). During that period the notions of Heaven Element, Earth Element, etc., (= unknowns x, y, etc.), together with allied notions of polynomials and methods of elimination, were introduced. Geometry was thus algebrized to be applied to solving of geometry problems. Numerous examples may be found in some still existant classics.

The algebrization of geometry was systematized owing to the creation of analytic geometry by R. Descartes. Descartes emphasized in his 1637 classic the geometry problem-solving rather than geometry theorem-proving which was the same spirit in ancient China. The analytic geometry also permits to prove geometry theorems by mere computations in contrast to the proving by purely geometrical reasoning of Euclid. This computational method of proving geometry theorems lacked however a general way of dealing with the associated system of equations usually in embarrassing confused form.

A turning point occurred in the time of Hilbert. In fact, in his 1899 classic there was some obscure passages which, after some clarification and extension, may be interpreted as a mechanical way of geometrical theoremproving. The proving, being computational and mechanical, can be carried out on a modern computer. A lot of difficult theorems have thus been proved on the computer in a straightforward and trivial way.

In recent years the Chinese mathematicians, mainly in MMRC (Math. Mech. Res. Center), have developed a general mechanization method for geometry theorem-proving and geometry problem-solving. Among the applications considered we may cite in particular:

1. Automated deduction of unknown relations and geometric loci.

2. Enumerative geometry and computational geometry.

3. Inequalities and optimization problems.

4. Mechanism studies.

5. CAGD: surface-fitting.

Numerous examples may be given to illustrate the various methods of geometry theorem-proving and geometry problem-solving, both old and new.