AIMing: Building Automated Reasoning System for Hyperbolic Geometry and Beyond

About This Grant

Automated theorem provers, which combine logical rules with creative input from artificial intelligence (AI), are rapidly advancing. These tools are particularly effective and efficient in Euclidean geometry, while extending these tools to other complex mathematical domains remains a major challenge. This project builds on the successful framework developed for Euclidean geometry and aims to create a novel reasoning system for hyperbolic geometry, a natural but more intricate domain with applications in physics and computer science. Advancing automated reasoning in this domain is expected to lead to a better understanding of the underlying principles of effective reasoning systems and pave the way for broader applications across research-level mathematics. A complementary goal of the project is the development of an innovative undergraduate course that introduces students to both the theory and practice of automated reasoning, guiding them in building their own basic theorem provers. The course will equip students with essential skills at the intersection of AI and mathematics, advancing STEM education, and strengthening leadership in scientific innovation. Broader impacts of the project include open-access software, instructional materials, and a machine-generated “Hyperbolic Geometry Encyclopedia” to support educators, students, and the research community. The project's main goals are to develop a robust automated reasoning system for hyperbolic geometry and to create a new undergraduate course on AI in mathematics. The investigators strive to achieve these goals by building upon their pre-developed prototype for Euclidean geometry, which will also serve as a core example for the new AI in mathematics course. A critical first step involves adapting the rule-based components of the reasoning system to incorporate the axioms of hyperbolic geometry. Based on these rigorous deductions, the investigators will generate a comprehensive dataset of hyperbolic geometry statements and their corresponding proofs, which will then serve as crucial training data for the artificial intelligence component of the system. This work is expected to yield a neuro-symbolic engine capable of automated theorem proving in hyperbolic geometry, with a long-term vision of extending these systems to even more complex geometries and mathematical domains. Combining the theoretical and educational aspects of this project, the investigators aim to empower current and future researchers with the necessary skill set and tools to leverage AI in mathematics. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.