Automated Discovery of Geometrical Theorems in GeoGebra

TL;DR

This paper introduces a prototype GeoGebra command called Discover that automates the analysis and discovery of geometric theorems in elementary planar geometry, emphasizing mathematical methods to manage complexity.

Contribution

It presents a new experimental tool for automated geometric theorem discovery within GeoGebra, including mathematical techniques to prevent combinatorial explosion.

Findings

Prototype successfully analyzes geometric figures for patterns and theorems

Methods to efficiently store and manage geometric properties

Potential for expanding automated geometric reasoning

Abstract

We describe a prototype of a new experimental GeoGebra command and tool, Discover, that analyzes geometric figures for salient patterns, properties, and theorems. This tool is a basic implementation of automated discovery in elementary planar geometry. The paper focuses on the mathematical background of the implementation, as well as methods to avoid combinatorial explosion when storing the interesting properties of a geometric figure.