Today I’m going to talk about using modern methods of algebraic geometry to automate (in large part) the proofs of statements of plane geometry. The discussion mostly follows Cox, Little, and O’Shea‘s “Ideals, Varieties, and Algorithms” which is a great book to use to learn the basics of algebraic geometry with lots of examples.
So we’re going to be looking in the polynomial ring over the complex numbers, , and we’ll first have to develop some machinery.
First, we must define a monomial ordering on to be any relation > on , or equivalently, any relation on the set of monomials , which is a total order, if and then , and is a well-ordering on . This means that every nonempty subset of has a smallest element under .
The three most important monomial orderings are lex, grlex, and grevlex. Lex is the lexicographic order, in this, if has positive first term. Grlex is the graded lexicographic order, in this, we define , and if and if , we use lex order. Grevlex is graded reverse lexicographic ordering. In this, if , and if then if the rightmost entry of is negative.
And here is some terminology: let and > a monomial ordering, then the multidegree of is
The leading coefficient of is , and the leading monomial of is . The leading term of is .
It turns out that this is enough to define a division algorithm on , which is analogous to the standard division algorithm:
Fix a monomial ordering on for all that follows and let be an ordered -tuple of polynomials.
Then every can be written , where is either zero or a polynomial which is not divisible by any of . We call the remainder of on division by . Furthermore, if then we have .
How do we proceed with this? Well, we first test the lead term of our polynomial for division by the lead term of . If it succeeds, we can perform monomial division, and then subtract the appropriate multiple of to cancel the lead term and repeat. If has lead term not divisible by , proceed to , etc. Unfortunately, this process depends on the order of division, and the remainder is not unique (in fact, it can be zero for some ordering and nonzero for another). There is, however, a way to patch this.
A finite subset of an ideal is said to be a Groebner Basis if . It shouldn’t be too surprising that this is the right notion, because the problem before would be if you got things that had lead term on the right but not the left.
It is a theorem that every ideal other than has a Groebner basis. Furthermore, any Groebner Basis for an ideal is a generating set of .
And so, the fact motivating Groebner bases, is that if we let be the remainder of upon division by , and is a Groebner Basis, then is independent of the ordering of , and iff .
So this solves the ideal membership problem, which is to determine whether a polynomial is in a given ideal (which corresponds to whether a function vanishes on a given variety, geometrically speaking).
Best of all, there is an algorithm for finding Groebner bases of ideals. First we define the -polynomial of nonzero. If and then let , where for each . We call the least common multiple of and , written
The -polynomial of and is .
This is in fact leading towards the notion of syzygy, which is where the comes from, and this concept is extremely important, though I won’t go into more detail in this post.
So now I’ll describe the Buchberger Algorithm.
Let be a polynomial ideal. Then we can extend to a Groebner basis by the following algorithm:
Output: a Groebner basis such that
Define , then let , and for each pair , Find . If then set . Do this until .
This algorithm is not optimal, but it works. We can shorten it by noticing that if two terms have relatively prime leading monomials, then the -polynomial must be zero, and by using other, more advanced, concepts.
We will use this machinery to give an example of what is called Automatic Geometric Theorem Proving. From here on, we will work with a very specific and simple example, and just note that everything done can be dealt with in more generality, and for harder problems (though you need more and more processing power to do it).Let be the vertices of a parallelogram in the plane. Then the diagonals and bisect each other at a point .
This is a fairly simple theorem in Euclidean geometry, and it will serve as an example here, because anything more interesting is too computationally intense and has polynomials that are too large to show off.
First we must translate this into polynomials. We place at the origin , and we will use for independent variables and for constrained variables. . , and .
Then the statements that the figure is a parallelogram are and . The denominators can be cleared and we get hypotheses and
Now we define , and the statements that is on both lines are and , and so we get and
We then use the Pythagorean Theorem to write the conclusions as polynomials, and
We then compute a Groebner basis for using lexicographic ordering with .
We get , where
The variety, that is, the set of common zeroes, is reducible, because , so denoting the variety of an ideal by , we have
In fact, , where
We note that on we have the equation , which causes our paralellogram to be a line, that is, degenerate. is also a degenerate case, where .
So, if the conclusions are zero on every point of , then they are true, and we can check this easily, by substituting values for the in the conclusions and , and then showing that the conclusions reduce to the zero polynomial, which they, in fact, do.