Carnegie Mellon University has been selected to lead a new national mathematics institute aimed at revolutionizing how researchers use artificial intelligence (AI) and machine learning to tackle complex scientific, economic, and security problems.
The Institute for Computer-Assisted Reasoning in Mathematics (ICARM), funded by the National Science Foundation (NSF) with additional support from the Simons Foundation, will explore how formal methods and AI can modernize mathematical reasoning. It is one of only six NSF-supported math institutes in the U.S. and will serve as a hub for advancing interdisciplinary research at the intersection of mathematics, computer science, and philosophy.
“Emerging technologies based on formal methods, AI and machine learning are transforming the landscape of mathematical research,” said Theresa Mayer, vice president for research at Carnegie Mellon. “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, professor of mathematical sciences and philosophy at CMU, the three-year pilot program will support collaborations across institutions and disciplines. “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,” Avigad said.
Researchers affiliated with ICARM will include faculty from CMU’s Mellon College of Science and School of Computer Science, as well as collaborators from the University of South Carolina and Georgia Gwinnett College. In addition to research, the institute will host summer schools, conferences, and workshops designed to build capacity and foster innovation in computer-aided reasoning.
Prasad Tetali, Alexander M. Knaster Professor and head of CMU’s Department of Mathematical Sciences, emphasized the broader potential of the 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.”
“Mathematical reasoning is foundational to many branches of science and engineering,” Tetali added. “When human insight and ingenuity are paired with machine-assisted formal reasoning, the scope of the outcome is limitless.”
Avigad described the NSF’s decision to fund ICARM as a “strong vote of confidence in its mission,” adding, “We are humbled by that trust, and we will do everything we can to make good on it.”
