Automatic geometry theorem-proving and automatic geometry problem-solving (Q4946075)

The present paper surveys work of the author and his colleagues in the MMRC (Math. Mech. Res. Center, Chinese Acad. of Sciences), on the topic of a general method of polynomial equation-solving. There are three sections in the paper; the first one actually states the method, which is based on a particular ordering of a finite set of polynomials in \(n\) unknowns, together with a well-ordering principle and two decomposition theorems (for zeroes and varieties). Not a single clue about the proofs is given, for further information it is referred to papers by various authors, but they are not cited in the text. The use of a particular ordering in the set of polynomials resembles the use of Gröbner bases, which are told to be equivalent to a special case of the introduced theory. In the second section some applications and examples are stated. The approach is based on different `principle methods' derived from the well-ordering principle and the decomposition theorems above. Several examples of problems in geometry are presented, and their solution is given, acknowledging the use of the method of polynomial equation-solving. The paper ends with a long section on historical discussions on the relationship between geometrical theorem-proving and geometrical problem-solving from the ancient Chinese mathematicians to Descartes. For the entire collection see [Zbl 0929.00067].