# Computer power in plane geometry

I often hear that modern computer programs "may prove any theorem in elementary Eucledian geometry". Of course, as stated it is false - say, they can not prove theorems about $n$-gons for arbitrary or large enough $n$, and so on. But I wonder, how really powerful are they in problems with not so many points, lines and circles. Morley's theorem is the often example of hard theorem, which may be easily proved by computer, but this does not impress me much, since Morley theorem has two free parameters, and some equality has to be proved. The question is how number of parameters, conditions on them and inequalities make the process of automatic proof slower. To make it more precise, let consider specific example.

Can any computer program prove Erdos-Mordell inequality?

-
I suspect the answer is Yes, and in particular if you ask Doron Zeilberger he'll gladly add a proof to his "geometry textbook downloaded from the future": math.rutgers.edu/~zeilberg/PG/gt.html :-) – shreevatsa Jul 18 '10 at 18:50
Alas, I do not see any inequality therein, and no theorem with hidden inequality (like Ptolemey inverse theorem). – Fedor Petrov Jul 18 '10 at 21:00

First off, I would be skeptical of the claim that computer programs "may prove any theorem in elementary Euclidean geometry", simply because it is so wide and general that is prone to be false. Secondly, I am not directly an expert in this field myself, but I hope my references are not too much off.

However, modern automatic geometric theorem proving is definitely capable of dealing with a large number of geometric problems, including those which involve geometric inequalities. The older methods (going back to Wu), translate a geometric statement is translated into an implication of the form $$\bigwedge_{i=1}^n f_i(x_1,\ldots,x_m) \implies f_0(x_1,\ldots,x_m)$$ where the $f_i$ are polynomials. From this, with various methods one then obtains a prove of the statement, or a counter example. I am suppressing here that often you need to specify further side conditions for a proof to be possible, e.g. that a triangle is non-degenerate; in fact, Wu's approach and the Gröbner basis even allow deducing sufficient conditions to make a theorem true in retrospect. The Wikipedia page for Wu's method gives some more details and a few references to relevant papers; you can easily google more.

Anyway, this allows encoding things like multiple points being collinear, points being contained on a circle, intersection of lines, perpendicularity of lines, and so on. However, this does indeed not allow encoding inequalities effectively; e.g. just specifying that a point is 'inside' a triangle, or that one value is less than another, in general is not possible.

But since Wu's original work, there have been many advances. If one looks a bit closer, then one notices that the above techniques actually prove theorems about complex geometry, as we are arguing about zeros of polynomials, and this all happens over an algebraically closed field. But we are usually interested in real geometry only. There are surprisingly many classical theorems from "real" geometry which remain true in the complex case, and this somewhat surprising (and as far as I know rather mysterious) fact ensures that nevertheless Wu's method and its relatives are quite successful. Still, people have worked on overcoming this limitation, as well as that of inequalities.

One approach is described "A New Approach for Automatic Theorem Proving in Real Geometry", by Dolzmann, Sturm & Weispfenning, who use quantifier elimination (from logic) to prove theorems in real geometry (as the title suggests), using their Reduce package Redlog. They use that, for example, to prove Pedoe's inequality. I am, however, not sure if this can be used to prove the Erdős–Mordell inequality; one could ask them. I think Sturm wrote his PhD thesis on the subject.

Another paper to look at is "A Practical Program of Automated Proving for a Class of Geometric Inequalities" by Lu Yang and Ju Zhang. There they describe a Maple package "Bottema" (unfortunately, this does not seem to be available on the net, at least I couldn't find it). They use it to prove a load of inequalities, and give many examples involving inequalities. To give you a flavor, here is an example (which they proved using their package):

Example 4. By $m_a$, $m_b$, $m_c$ and $2 s$ denote the three medians and perimeter of a triangle, show that $$\frac{1}{m_a}+\frac{1}{m_b}+\frac{1}{m_c}\geq > \frac{5}{2}.$$

And here is another excerpt (I included it as it also goes back to Erdős).

A. Oppenheim studied the following inequality in order to answer a problem proposed by P. Erdös.

Example 9. Let $a$, $b$, $c$ and $m_a$, $m_b$, $m_c$ denote the side lengths and medians of a triangle, respectively. If $c = \min\{a, b, c\}$, then $$2m_a+2m_b+2m_c \leq 2a+2b+(3\sqrt{3}-4)c.$$

This all does not answer your question about the Erdős–Mordell inequality. And I am afraid I don't know the answer! But I hope my above explanations at least made it plausible that the answer could be yes, however vague that statement is.

-
The link to Wu's method on wikipedia is not working for me. Can you please check the link? – KConrad Aug 18 '10 at 1:23
I fixed that last night, please let me know if you spot any other problems :) – Max Horn Aug 18 '10 at 9:38