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+(3sqrt{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.
No comments:
Post a Comment