Is it true that all of the euclidean geometry problem in the IMO(international mathematical olympiad) could all be solve by the analytical geometry?

Question

Is it true that all of the euclidean geometry problem in the IMO(international mathematical olympiad) or even generalize to say that all the plane geometry problem and 3d-geometry could be solve by the analytical geometry/algebraic geometry?

Answer 1

By an old result of Tarski, the elementary theory of real-closed fields is decidable. A great many problems in elementary geometry, including the typical IMO geometry problems, can be stated, via coordinatization, as sentences in the language of real-closed fields.

Tarski's general decision procedure can therefore be in principle applied to solve such problems.

There has been a certain amount of theoretical and practical implementation work done on the problem. Seidenberg and Cohen gave alternate approaches.

Answer 2

Some of the Chinese teams to the IMO were trained in the use of the "area method", which is a simplified form of (complex number) quantifier elimination adapted to plane geometry, developed and popularized in China, and implemented in geometric theorem-proving software. The generality of the method is limited compared to full quantifier elimination, but it can handle any geometry problem where the configuration is constructible from a finite set of starting points by ruler and compass. For theorems that require more complicated constructions or need the coordinates to be real (so as to have order properties such as two sides to every line) the area method can still be of some use but will not solve the problem completely by itself.

An earlier and more general technique, not suitable for hand calculation but implemented as theorem proving software, is Wu's method, which in computer algebra terms is "ideal membership testing" using Groebner bases. It tests whether the equations defining the diagram in the statement of a geometry theorem imply the equation that expresses the theorem's conclusion.

If you have a full quantifier elimination engine (over $\mathbb{R}$) then any Euclidean geometry problem based on a finite number of points, lines, circles and straight-line distances, can be solved automatically. This is the Tarski theorem and was part of his work on axiomatization of first-order Euclidean geometry.