Teaching Geometric Proof with Tech: Pitfalls and Possibilities

Geometric proof is a foundational yet notoriously difficult topic in mathematics, requiring students to integrate visual, logical, and notational skills. While educational technology has transformed other areas of math, its impact on proof-solving remains limited. To understand this gap, the authors conducted semi-structured interviews with 18 experienced geometry teachers to identify their pedagogical goals and technological requirements. They then reviewed 33 commercial and research tools to evaluate how well current software supports the actual proof-solving workflow.

The study reveals a critical disconnect between teacher needs and available software. Teachers view geometric proof as a highly visual, iterative process where students must constantly annotate diagrams to track known information and identify patterns. Current digital tools, however, treat diagrams as static images or rigid, automated components. Because existing software lacks the flexibility to allow students to manually mark up diagrams as they work, teachers frequently revert to traditional pen-and-paper, which supports these essential visual-logical connections.

To bridge the gap between classroom reality and technology, the authors propose four design pillars for the next generation of proof tools:

• Integrated Diagramming: Tools must treat the diagram as a dynamic, semantically linked component of the proof, allowing students to add and verify annotations that update the logical state.
• Automated Scaffolding: Systems should use specialized theorem provers to generate problems and provide contextual feedback, reducing the manual burden on teachers.
• Format Flexibility: Software should support multiple proof representations (e.g., flowcharts, paragraph proofs) to help students understand that proofs can have multiple valid logical paths.
• Reduced Accidental Complexity: Designers must prioritize intuitive user experiences to ensure that students focus on the essential complexity of the geometric argument rather than navigating clunky software interfaces.