Finding and proving new geometry theorems in regular polygons with dynamic geometry and automated reasoning tools

Abstract

In 1993 Watkins and Zeitlin published a method [1] to simply compute the minimal polynomial of cos (2 π/ n), based on the Chebyshev polynomials of the first kind. For the work presented in this paper we have implemented a small augmentation, based on Watkins an Zeitlin’s work, to the dynamic mathematics tool GeoGebra. We show that this improves GeoGebra’s capability to discover and automatically prove various non-trivial properties of regular n-gons. Discovering and proving, in this context, means that the user can sketch a conjecture by drawing the geometric figure with the tools provided by GeoGebra. Then, even if the construction is just approximate, in the background a rigorous proof is computed, ensuring that the conjecture can be confirmed, or must be rejected. In this paper the potential interest of automated reasoning tools will be illustrated, by describing such new results in detail, obtained by some recently implemented features in GeoGebra. Besides confirming well known results, many interesting new theorems can be found, including statements on a regular 11-gon that are impossible to represent with classical means, for example, with a compass and a straightedge, or with origami.