# AIMing: Building Automated Reasoning System for Hyperbolic Geometry and Beyond

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · Brown University (RI) · $800,000

## Abstract

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

## Key facts

- **NSF award ID:** 2522850
- **Awardee organization:** Brown University (RI)
- **SAM.gov UEI:** E3FDXZ6TBHW3
- **PI:** Peter Zenz
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), EXP PROG TO STIM COMP RES
- **Estimated total:** $800,000
- **Funds obligated:** $800,000
- **Transaction type:** Standard Grant
- **Period:** 09/01/2025 → 08/31/2028

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2522850

## Citation

> US National Science Foundation, Award 2522850, AIMing: Building Automated Reasoning System for Hyperbolic Geometry and Beyond. Retrieved via AI Analytics 2026-06-08 from https://api.ai-analytics.org/grant/nsf/2522850. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*