Progress in the area of automated theorem proving has been traditionally demonstrated by automatically and mechanically proving conjectures and theorems in classical mathematics. Examples include the proof of the four-color theorem and, more recently, the proof of Kepler’s conjecture. Following tradition, the authors of the current paper demonstrate their technique by proving Morley’s theorem, which states: in any triangle, the three points of intersection of the adjacent angle trisectors form an equilateral triangle.

This theorem was discovered in 1899, and was so unexpected that it was known as “Morley’s miracle.” A number of simplifications have been achieved over the years, and the current paper distills the essence of these simplifications into a general technique for proving a class of theorems in geometry.

The technique itself is very simple and appeals to no more than elementary properties of angles and triangulations. The technique is suitable for mechanization, and the authors have implemented the algorithm in a tool. The algorithm also seems to require no more than simple symbol matching, perhaps using standard unification techniques, and elementary arithmetic.

On the flip side, this technique does seem to be quite specialized and there does not seem to be a clear understanding of the problems that it can solve. However, it seems quite suitable to be incorporated as a simplification tactic in existing frameworks like Coq, HOL, and so on, where it is quite likely to have some effect.