In recent 20 years, great progress has been made in the research and practice of mechanical proof of geometric theorems. From an ancient dream to an amazing breakthrough, it is the dream of some outstanding scientists in history to establish a universal geometric problem-solving method, solve problems in batches and even prove everything. To this end, Descartes invented the coordinate system; Leibniz imagined a reasoning machine; Hilbert gave the mechanization theorem of a class of geometric propositions in his famous work "Geometric Basis". The emergence of electronic computers has promoted the mechanization of mathematics. In 1950s, Taskey proved the possibility of mechanization of elementary geometry by algebraic method. By the 1960s, Slug and Moses had realized symbolic integration, and the mechanization of algebraic and analytical calculation problems had begun to take shape, but the mechanical proof of geometric theorems seemed far away. Then, Grant and others proposed to establish a geometric inference engine by logical method, and Collins and others improved Taskey's algebraic method. Until 1975, there is still no effective algorithm for judging nontrivial geometric propositions by computer. Just as the enthusiasm in this field is often neglected because of the slow progress, the proposal of Wu Wenjun method has brought great vitality to the research of theorem machine proof. Wu Faneng can quickly prove difficult geometric theorems on a microcomputer. Zhou Xianqing developed Wu Fa, realized it as an effective general program, proved 5 12 nontrivial theorems, and wrote them into English monographs. This progress is a major breakthrough in the field of automatic reasoning and is praised as a revolutionary work by international counterparts. The success of Wu's method from machine judgment to automatic generation of readable proof makes the research on machine proof of geometric theorems, which was once ignored, active. It is very important to prove the direction of geometric theorem by algebraic method. New algebraic methods emerge one after another. In foreign countries, Zhou Xianqing and others put forward the algorithm and program of constructing geometric theorem machine proof by Grobner basis method, and achieved success. In China, Hong Jiawei put forward the theory of single-point illustration, but it is too complicated to realize. Zhang Jingzhong and Yang Lu put forward the numerical parallel method, and realized the machine proof and machine invention of nontrivial geometry theorem on low-level microcomputers (even calculators). The advantage of numerical parallel method is that it needs little memory and is easy to parallelize. These methods all belong to algebraic methods. Their presentation and realization enrich the research on mechanical proof of geometric theorems. But compared with wo fat, there is no big new breakthrough. What the algebraic method can't satisfy is that the proof it gives is about the complex calculation of large polynomials, and it is difficult for people to understand its geometric meaning and test whether it is correct. Whether the concise and ingenious computer-generated proof, the so-called readable proof, can be understood and easily tested is a challenging topic in the fields of automatic reasoning and artificial intelligence. Some famous scientists believe that the basic idea of machine proof is to replace qualitative difficulty with quantitative complexity, which makes it unimaginable for machine to generate readable proof. Some foreign scholars have been working on the automatic generation of readable proofs of geometric theorems since the 1960s. Over the past 30 years, they have made little progress and failed to give an effective algorithm and program for machine proof of even a small class of nontrivial geometric theorems. Based on the new geometric method developed for many years, the author puts forward the idea of eliminating points. In cooperation with Zhou Xianqing and Gao Xiaoshan, this difficulty was broken through in 1992, and the readable proof of geometric theorem was automatically generated. This new method is neither based on coordinates nor different from the traditional synthesis method, but an open system formed by combining geometry, algebra, logic and artificial intelligence methods with geometric invariants as tools. It selects several basic geometric invariants and a set of drawing rules, and establishes a series of vanishing point formulas related to these invariants and drawing rules. When the premise of the proposition is input in the form of drawing sentences, the program can call the appropriate elimination formula to eliminate the constraint points in the conclusion one by one, and finally get to the bottom of it. The combination of the process record of vanishing point and vanishing point formula is a proof with geometric significance. The algorithm is complete for constructive equality geometry proposition, but its application scope is not limited to this kind of proposition. The program based on this method has automatically generated hundreds of concise and readable proofs of difficult geometric theorems on the microcomputer, and its efficiency is higher than other methods. With the different geometric quantities used, various styles of proofs can be generated, such as area method, vector method, complex number method, full angle method, etc., and can also be used in solid geometry. Yang Lu, Gao Xiaoshan and Zhou Xianqing cooperated with the author to apply vanishing point method to the automatic generation of readable proofs of non-Euclidean geometry, and obtained a number of new non-Euclidean geometry theorems. The elimination point method can also be used for geometric calculation and formula derivation. Establishing a new principle based on the idea of geometric quantity and vanishing point is like opening a deposit solved by a geometric theorem machine. It also makes it possible to apply the mechanical proof results of geometric theorems in mathematics education. This achievement is praised by international peers as a milestone in the development of enabling computers to handle geometry like arithmetic, and it is the most important work in the field of automatic reasoning in the past 30 years. In most cases, the vanishing point method can also prove the extraordinary theorem with paper and pen. It ended the situation that there was no definite proof method for geometric problems for two thousand years, and promoted the method of solving elementary geometric problems from the level of four miscellaneous problems to the stage of algebraic equations. A new stage in which machine proofing is comparable to manual proofing. However, compared with the colorful geometric knowledge accumulated by human beings for thousands of years, what computers can do at present is still very limited. More methods mastered by geometricians should be taught to computers, so that the solutions generated by computers can be compared with those generated by geometricians. For this reason, it is necessary to analyze what methods the geometer has to solve problems and what knowledge the computer has learned to determine what to do next and how to do it. Geometricians often use the following four methods: W 1. Test: observe and calculate the specific figures to determine that the proposition is true. W2。 Search: according to common lemmas and known conditions, find more geometric properties in the title map. If this does not achieve the goal, then the information obtained is the basis for further work. W3。 Reduction: starting from the conclusion, using the known information, eliminating the dependent geometric quantities or geometric elements, so that the truth of the conclusion tends to be obvious or easy to test. W4。 Transformation: changing the form of propositions, such as geometric transformation, reduction to absurdity, auxiliary lines, etc. The machine simulation of method W 1 is realized. The mechanization research of means W3 has achieved the greatest success. Wu method, national standard method, area method and vector method all belong to this category. It means that W4 fully embodies the flexibility and richness of human thinking activities, and it is still difficult to be mechanized. Means W2, search, is a conventional method in traditional geometric proof activities, and it is the basis of the supplement and transformation of transformation. A geometric information search system (GISS) based on forward push mode is designed and implemented. Due to the proper selection of geometric tools, reasonable data organization and optimized reasoning process, the effect is excellent. The problem of using search method to deal with propositions involving circles and find out all possible geometric properties (reaching the fixed point of reasoning) in literature has been satisfactorily answered by our algorithm. Our program is implemented in C language on the next workstation. It is used for 16 1 nontrivial geometric propositions, all of which reach the fixed point in a reasonable time, and we can find new theorems and prove results that other methods can't prove. This program has the function of adding some auxiliary lines. Research on Nonlinear Algebraic Equations The realization of machine-generated readable proofs will not make algebraic methods worthless. Some special problems and geometric problems of algebraic curves and surfaces still need to be solved by algebraic methods. Algebraic method is closely related to the theoretical and symbolic solutions of nonlinear algebraic equations, and is widely used, which is a hot spot of automatic reasoning. Many problems in mathematics, physics and engineering technology depend on solving algebraic equations in the final analysis. Linear equations are easy to handle, but nonlinear equations are difficult. Especially the symbolic solution of nonlinear equations is more difficult and important in theory. In the19th century, people put forward various resultant methods to study nonlinear algebraic equations. Because the combination method involves the calculation of large determinant, the research is cold. With the appearance of computers in this century, people have studied new algorithms. In 1960s, GB method and Ritt method were put forward abroad. GB method is a complete method. Ritt method has been improved by Mr. Wu Wenjun and has become a complete method. It is called Ritt-Wu method, and it is called Wu method for short in China (using Ritt-Wu method to prove geometric theorems by machine is also called Wu method. Some people abroad call the Wu method of machine proof Ritter-Wu method, which is inaccurate. Ritter has nothing to do with the mechanical proof of geometric theorems. )。 There is no conclusion about which of the two methods is better. For the machine proof of geometric theorems, Wu method is indeed superior to the national standard method. Chinese scholars have also solved many important problems with Wu method, involving theoretical physics, differential equations, spline theory and robots. Although there are excellent and complete methods such as Wu method and national standard method, more difficult problems need more powerful new methods. In recent years, foreign countries have put forward new ideas and algorithms many times, and Europe has also invested millions of dollars to organize projects to study the solutions of nonlinear algebraic equations, but there has been no breakthrough. Recently, based on our new theory and new algorithm-resultant matrix method, Fu compiled MAPLE program for symbolic solution and machine proof of algebraic equations. The characteristics of the new algorithm are: (1) the complete method of symbolic solution and compatibility judgment of nonlinear algebraic equations. ⑵ Does not depend on the factorization of polynomials. ⑶ Using the weak nondegenerate condition of zero decomposition to reduce redundant branches. (4) The sub-resultant calculation is combined with numerical experiments to eliminate elements in a large range. 5] decompose the given equation into trigonometric series, which is convenient for computer proof and final solution. Through example calculation, this method has better effect than other known methods. This method can solve the six-variable cyclic equation on PC486 and solve all kinds of six-joint robot problems in reverse, which is impossible by other methods. Another new development in the study of nonlinear algebraic equations is the discriminant system of algebraic equations with real coefficients proposed by Yang Lu and others, which not only completely solves a basic problem about algebraic equations that has been unresolved for centuries, but also makes a breakthrough in the mechanical proof of geometric inequalities. The program recently written by Yang Lu and others can quickly prove many geometric inequalities, deduce geometric inequalities according to given conditions, and correct and improve some foreign results about geometric inequalities. Prospects and Suggestions It is expected that in the next ten years, the machine solution of elementary geometric equality problems will be basically completed and will enter the practical stage. On the basis of the above achievements, new hot spots will appear:

(1) Under the influence of automatic generation of readable proofs of geometric theorems, new progress has been made in the research of machine solution with geometric invariants as tools. For example, the machine solution of geometric drawing, the research of geometric reasoning database, and the research of readable proof of differential geometry.

⑵ With the development of real algebra, there will be a new breakthrough in solving geometric inequalities by machines.

⑶ The theory and algorithm of nonlinear algebraic equations will remain a hot topic. More attention will be paid to parallel algorithms, such as resultant and interpolation.

⑷ Research on machine derivation of differential polynomials.

The results of machine proof, especially the research results of the theory and algorithm of nonlinear algebraic equations, will be more applied to the fields of mathematics, physics and engineering technology. At present, China is in the leading position in the world in the mechanical proof of geometric theorems.

In the research field of nonlinear algebraic equations, the competition is fierce. China has entered the advanced ranks, but it can't be said that it is ahead. In the development of mathematical mechanization software, China lags far behind the advanced countries in Europe and America because of its late start, small team and insufficient funds. We should not be content to be ahead in some ways. While continuing to study the machine proof of geometric theorems and keeping ahead, we should concentrate on the direction of nonlinear algebraic equations, especially on the research of practical and effective algorithms. In the popularization and application of mathematical mechanization, we should also invest our strength, give play to the advantages of theory and algorithm, and catch up with the advanced software development. On the basis of the results of machine proof of geometric theorem, we will develop high-intelligence educational software and symbolic calculus mathematical software with independent copyright, and make contributions to China's science, technology and education. This paper is a detailed summary of the special report made by the author at the 9th National Academic Conference of China Computer Federation.