AIMing: AI Theorem Proving Beyond Limited Data: Efficient Learning of Mathematicians' Ecosystem

About This Grant

Mathematical breakthroughs have historically driven advances in technology, national security, and economics. Examples of these breakthroughs include cryptography methods that protect digital infrastructure or algorithms that power modern computing, such as planning, supply chain, and navigation optimization. However, the pace of mathematical discovery is limited by the capacity of human mathematicians to explore increasingly complex problems. This project addresses a critical need by developing artificial intelligence (AI) systems that can accelerate mathematical research and theorem proving at scale. The goal is to create the first AI system capable of proving graduate-level mathematical theorems and tackling unsolved problems that challenge even world-class mathematicians. One motivating observation is that current AI systems for theorem-proving are trained in a way vastly different from how mathematicians learn. In reality, mathematicians develop their skills by working collectively within an ecosystem by taking on different roles at various times. Mathematicians also specialize in various areas and skill sets while actively collaborating across areas to build connections and transfer knowledge. The key approach is to train AI systems that imitate the evolution and interactions of mathematicians. This research would serve the national interest by accelerating scientific discovery across fields that depend on advanced mathematics, from quantum computing and cybersecurity to materials science and economics. It will also produce new techniques for training AI systems with limited high-quality data, a challenge that extends far beyond mathematics, such as scientific discovery research, medical diagnosis, and national defense applications. The project will also strengthen American competitiveness in AI by training the next generation of researchers through new coursework and mentorship programs, while making all developed tools freely available to the broader scientific community. This project addresses a fundamental limitation in automated theorem proving: while current large language models (LLMs) can solve International Mathematical Olympiad problems and college-level theorems, they remain unable to prove graduate-level theorems or tackle conjectures that challenge world-class mathematicians. The hypothesis is that existing AI systems are fundamentally different from how mathematicians develop expertise, which is through collaborative ecosystems with diverse roles and cross-field knowledge transfer. The project’s goal is to train multiple LLMs to simulate the mathematicians' learning, ideation, specialization, interaction, and cross-pollination process. Furthermore, they will enhance these neural models—which are good at capturing human intuition and insights—with software tools such as search and Python executors, in a computationally efficient manner, enabling AI to surpass human capabilities. Concretely, the project has the following three thrusts. In Thrust 1 (Learning Roles of Mathematicians), LLMs will be trained to take on various roles, such as conjecturers, provers, reviewers, agenda setters, and synthesists, while providing supervising signals to each other. In Thrust 2 (Specialization, Cross-Field Unification, and Knowledge Transfer), expert models will be trained using customized state representations and design higher-level or merged provers that address more general mathematical problems by leveraging the efficiency of the individual provers in a unified framework. Finally, in Thrust 3 (Scalable Serving and Training Systems), the project will innovate various efficiency optimization techniques for inference-time search, reward assignments, and high-throughput serving infrastructure. The expected contributions include an AI theorem-proving tool that transforms mathematical research by enabling a systematic way to explore and validate complex proofs across disciplines. This tool could accelerate mathematical discovery, providing a powerful mechanism for testing, validating, and extending mathematical knowledge. Moreover, the findings on learning from limited data and the ecosystem of AI-based mathematicians can be generalized to other adjacent domains, such as physics and computer science. 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.