  Geometry theorem proving forms a major and challenging component in the K-12
mathematics curriculum. A particular difficult task is to add auxiliary
constructions (i.e, additional lines or points) to aid proof discovery.
Although there exist many intelligent tutoring systems proposed for geometry
proofs, few teach students how to find auxiliary constructions. And the few
exceptions are all limited by their underlying reasoning processes for
supporting auxiliary constructions. This paper tackles these weaknesses of
prior systems by introducing an interactive geometry tutor, the Advanced
Geometry Proof Tutor (AGPT). It leverages a recent automated geometry prover to
provide combined benefits that any geometry theorem prover or intelligent
tutoring system alone cannot accomplish. In particular, AGPT not only can
automatically process images of geometry problems directly, but also can
interactively train and guide students toward discovering auxiliary
constructions on their own. We have evaluated AGPT via a pilot study with 78
high school students. The study results show that, on training students how to
find auxiliary constructions, there is no significant perceived difference
between AGPT and human tutors, and AGPT is significantly more effective than
the state-of-the-art geometry solver that produces human-readable proofs.
