Computer-Generated Geometry Proofs in a Learning Context

Given its formal, logical, and spatial properties, geometry is well suited to teaching environments that include dynamic geometry systems (DGSs) , geometry automated theorem provers (GATPs), and repositories of geometric problems. These tools enable students to explore existing knowledge in addition to creating new constructions and testing new conjectures. In this chapter, we trace the evolution of current automatic proving technologies, how these technologies are beginning to be used by geometry practitioners in general to validate geometric conjectures and generate proofs with natural language and visual rendering, and foresee their evolution and applicability in an educational setting.