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