Impressive progress has recently been made in the field of automated geometry theorem proving. The main technique works as follows: let T be a geometric conjecture. One chooses a suitable coordinate system and translates the conjecture T into an equivalent algebraic statement A. Applying methods of computational algebraic geometry, one tries to prove or to reject the algebraic statement A. It might well happen, however, that the theorem proving system returns an answer stating the truth of the conjecture provided an additional algebraic assumption is satisfied. Hence, the problem arises of determining the geometric meaning of the returned assumption. This paper presents new theoretical background that might lead to new automated systems that translate algebraic conditions into geometric ones.

The authors conceptually follow the approach of White [1], who presented a partial solution to this question based on invariant theoretic reasoning in projective geometry. In a projective space, every synthetic geometric construction can be presented using meets and joins of points. Translating into the Cayley algebra, one obtains an equation that may be expanded into the algebra of invariants. This transformation finally yields a homogeneous bracket polynomial having integer coefficients. Conversely, if one can factor every bracket polynomial with integer coefficients that is homogeneous in the occurrence of each point into simple Cayley expressions in meet and join, then one obtains a synthetic construction. Even deciding whether a given bracket polynomial is Cayley factorable is extremely difficult, however. While White’s algorithm solves the multilinear case, this paper deals with the general case. In particular, the following remarkable result is proven. For every homogeneous bracket polynomial P of rank r ≥ 3 a monomial M exists such that the product PM can be factored into a meet and join expression. Moreover, the proof of the factorization theorem yields a linear degree bound for M. The main tool in the construction is an algorithm for rewriting polynomial functions in terms of synthetic constructions.

Although this theorem is still too general to be directly applied for finding geometric meanings of algebraic expressions, it gives more evidence that Cayley factorization might play an increasing role in future geometric computer algebra systems. The paper is well written and contains several nice examples that shed additional light on the problems and their solution.