Discovering geometry theorems in regular polygons

Abstract

By using a systematic, automated way, we discover a large amount of geometry statements on regular polygons. Given a regular n-gon, its diagonals are taken, two pairs of them may determine a pair of intersection points that define a segment. By considering all possible segments defined in this way, we can compute the lengths of them symbolically, and, depending on the simplicity of the symbolic result we classify the segment either as “interesting” or “not interesting”. Among others, we prove that in a regular 11-gon with unit sides the only rational lengths appearing the way described above, are 1 and 2, and the only quadratic surd is 3. The applied way of proving is exhaustion, by using the freely available software tool RegularNGons, programmed by the author. The combinatorial explosion, however, calls for future improvements involving methods in artificial intelligence. The symbolic method being used is Wu’s algebraic geometry approach [1], combined with the discovery algorithm communicated by Recio and Vélez [2]. The heavy computations are performed by a recent version of the Giac computer algebra software, running in a web browser with the support of the recent technology WebAssembly. Visual communication of the obtained results is operated by the dynamic geometry software GeoGebra.