Mathematical Olympiad problems can be used to evaluate the performance of theorem
provers. In solid geometry, three general-purpose theorem proving methods are evaluated: the characteristic
set method, the Gr¨obner basis method, and the vector algebra method. All perform well
in testing the problems of solid geometry collected in the encyclopedia [19], the main difference
being the geometrical interpretability of the additional non-degeneracy conditions. Some problems
in the past Mathematical Olympiad contests are found to need minor or even major repair to be
correct.