Symbolic Comparison of Geometric Quantities in GeoGebra

TL;DR

This paper introduces GeoGebra's new Compare command, enabling automatic conjecture generation and proof of geometric equalities and inequalities, enhancing secondary education and supporting experimental exploration in planar geometry.

Contribution

The paper presents a novel Compare feature in GeoGebra that automates conjecture formation and proof, including inequalities, for educational and research purposes.

Findings

Supports automatic conjecture and proof in geometry

Works efficiently on standard personal computers

Enables discovery of new geometric results

Abstract

Comparison of geometric quantities usually means obtaining generally true equalities of different algebraic expressions of a given geometric figure. Today's technical possibilities already support symbolic proofs of a conjectured theorem, by exploiting computer algebra capabilities of some dynamic geometry systems as well. We introduce GeoGebra's new feature, the Compare command, that helps the users in experiments in planar geometry. We focus on automatically obtaining conjectures and their proofs at the same time, including not just equalities but inequalities too. Our contribution can already be successfully used to support teaching geometry classes at secondary level, by getting several well-known and some previously unpublished result within seconds on a modern personal computer.