# An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development

arXiv: https://arxiv.org/abs/2509.02758 · HTML: https://mlsanity.com/paper/2509.02758/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Spatial and embodied reasoning, one of 17 directions in LLM reasoning.
- Builds on 6 of its 33 references that are in the map.
- First posted on arXiv 2 Sep 2025.

## Placed in

- LLM reasoning / [Spatial and embodied reasoning](https://mlsanity.com/lr/spatial-and-embodied-reasoning/)

## Builds on (most cited first, 6 of 6)

- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [LeanGeo: Formalizing Competitional Geometry problems in Lean](https://mlsanity.com/paper/2508.14644/) (2025)
- [Lean-auto: An Interface between Lean 4 and Automated Theorem Provers](https://mlsanity.com/paper/2505.14929/) (2025)
- [OntoMathPRO Ontology: A Linked Data Hub for Mathematics](https://mlsanity.com/paper/1407.4833/) (2014)

## Abstract (arXiv)

Euclidean geometry has historically played a central role in cultivating logical reasoning and abstract thinking within mathematics education, but has experienced waning emphasis in recent curricula. The resurgence of interest, driven by advances in artificial intelligence and educational technology, has highlighted geometry's potential to develop essential cognitive skills and inspired new approaches to automated problem solving and proof verification. This article presents an ontology-based framework for annotating and optimizing geometry problem sets, originally developed in the 1990s. The ontology systematically classifies geometric problems, solutions, and associated skills into interlinked facts, objects, and methods, supporting granular tracking of student abilities and facilitating curriculum design. The core concept of 'solution graphs': directed acyclic graphs encoding multiple solution pathways and skill dependencies enables alignment of problem selection with instructional objectives. The framework has been tested in practice through the annotation of thousands of problems over three decades. We contend that our approach addresses longstanding challenges in representing dynamic, procedurally complex mathematical knowledge. We conclude by articulating a research agenda: the open problems of automated problem annotation and solution validation, whose resolution would reduce the time teachers spend validating student work and enable interactive feedback for self-learners.