Collaborative Research: AIMing: Synergistic Advancement of AI and Mathematics

This collaborative research project aims to synergize advancements in artificial intelligence (AI) and mathematics to enhance computational methods for mathematical reasoning and expedite mathematical discovery. The project brings together a team of experts from the mathematical sciences, computer science, and AI, leveraging their complementary skills to tackle complex problems in these intersecting fields. The research will focus on developing AI models that can reason constructively about complex mathematical problems, improving formal proof systems, and creating new AI tools that integrate mathematical intuition and creativity. Additionally, the project seeks to advance AI with mathematical foundations, aiming for more interpretable, controllable, and trustworthy AI models. By addressing both the advancement of mathematical research through AI and the enhancement of AI with mathematical insights, the project aims to create significant breakthroughs in both areas, ultimately contributing to broader societal impacts and scientific knowledge. More specifically, this project investigates how to endow AI systems with the ability to reason constructively and intuitively about complex mathematical problems, using techniques from reinforcement learning, generative modeling, and formal proof verification. Central to the research is the modeling of theorem proving as a sequential decision-making process, where formal proofs are framed as trajectories through combinatorially structured state and action spaces. The team will develop scalable task embeddings to quantify the complexity and diversity of reasoning tasks, enabling curriculum learning strategies and improved training data generation. Ideas from intrinsic motivation such as novelty and surprise will guide proof-space exploration in settings where reward signals are sparse or delayed. The project also aims to construct interpretable and elegant proofs by identifying efficient trajectories through the reasoning space, aligned with human-interpretable landmarks, and to develop alignment metrics for selecting models suited to specific problem types. In parallel, the team will investigate the mathematical foundations of neural architectures, analyzing the representational power and optimization of transformer-based models in formal reasoning contexts. Generative models will be applied to construct counterexamples and structured mathematical objects, providing tools for discovery in mathematical domains such as knot theory, group theory, and algebraic geometry. Through these integrated efforts, the project seeks to advance both the development of mathematically grounded AI systems and the use of AI as a tool for mathematical research. 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.