TLDR: Carnegie Mellon University has established the Institute for Computer-Aided Reasoning in Mathematics (ICARM), a new national institute backed by the National Science Foundation (NSF) and the Simons Foundation. This three-year pilot program aims to revolutionize mathematical discovery and problem-solving by integrating artificial intelligence (AI) and formal methods, addressing complex challenges in science, economics, and security.
Pittsburgh, PA – Carnegie Mellon University (CMU) has announced the launch of a groundbreaking national initiative, the Institute for Computer-Aided Reasoning in Mathematics (ICARM). This new institute, significantly supported by the National Science Foundation (NSF) and with additional funding from the Simons Foundation, is set to transform the landscape of mathematical research by harnessing the power of artificial intelligence (AI) and machine learning.
ICARM is one of only six NSF-supported mathematics institutes across the United States, positioning CMU at the forefront of interdisciplinary research at the intersection of mathematics, computer science, and philosophy. The institute’s core mission is to explore how formal methods and AI can modernize mathematical reasoning, making it faster, more reliable, and applicable to pressing challenges in various fields, including science, cybersecurity, finance, and healthcare.
Theresa Mayer, Vice President for Research at Carnegie Mellon, emphasized the significance of this development, stating, “Emerging technologies based on formal methods, AI and machine learning are transforming the landscape of mathematical research. We are grateful to the National Science Foundation for its leadership in establishing ICARM and recognizing the importance of this moment.”
Led by Director Jeremy Avigad, a distinguished professor of mathematical sciences and philosophy at CMU, ICARM will operate as a three-year pilot program. Professor Avigad highlighted the institute’s focused approach: “The institute will focus on the mathematical components of these tasks and use the technologies to support mathematical reasoning and computation in all its applications.” This includes developing AI models capable of conjecturing, proving, and visualizing complex theorems, bridging the gap between symbolic reasoning and neural networks.
The institute will foster extensive collaborations, bringing together faculty from CMU’s Mellon College of Science and School of Computer Science, alongside researchers from partner institutions such as the University of South Carolina and Georgia Gwinnett College. Beyond research, ICARM is committed to building capacity and fostering innovation through various educational initiatives, including summer schools, conferences, and workshops.
Also Read:
- Allen Institute for AI Secures $152 Million from NSF and NVIDIA to Advance Open AI for Scientific Research
- New Academic Initiatives and Industry Focus Drive Advancements in Artificial Intelligence Models
Prasad Tetali, Alexander M. Knaster Professor and Head of CMU’s Department of Mathematical Sciences, underscored the broader societal impact envisioned for the institute’s work. “While a focus of the institute will be on facilitating research in mathematical sciences, my hope is that the developed technologies will also play a crucial role in significantly improving the way mathematics can be taught in schools and colleges,” Tetali remarked. This initiative is a key component of Carnegie Mellon’s broader AI research strategy, which also encompasses work on verifying software systems and modeling complex systems through computation.


