image of a man at a podium

New NSF Institute at CMU Will Help Mathematicians Harness AI and Advance Discoveries

By Lucy Perkins Email Lucy Perkins

Cassia Crogan

A new federally funded national institute at Carnegie Mellon University will help mathematicians use artificial intelligence to make mathematical reasoning faster and more reliable in solving pressing challenges across science, security and the economy.

With an investment from the National Science Foundation (NSF) and additional support from the Simons Foundation, the Institute for Computer-Aided Reasoning in Mathematics (ICARM) — one of just six mathematics institutes across the U.S. to receive NSF support — will help researchers modernize mathematical reasoning to strengthen real-world problem solving in domains like cybersecurity, finance, space and health care.

The institute kicks off at a crucial moment as the mathematical community learns to incorporate new technology into its work.

portrait of Theresa Mayer

“Emerging technologies based on formal methods, AI and machine learning are transforming the landscape of mathematical research,” said Theresa Mayer, vice president for research. “We are grateful to the National Science Foundation for its leadership in establishing ICARM and recognizing the importance of this moment. As host of the new institute, Carnegie Mellon is committed to supporting the mathematical sciences community through deep interdisciplinary collaboration and new frameworks for advancing fundamental discovery.”

Machine learning provides ways of detecting subtle mathematical patterns, which is helpful for everything from discovering drugs to predicting financial markets. Formal methods and automated reasoning are used to ensure that software systems perform correctly.

“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,” said Jeremy Avigad, director of ICARM and professor in the Department of Mathematical Sciences and the Department of Philosophy at CMU. 

ICARM also will provide opportunities such as summer schools, workshops and a conference to explore the use of these technologies in mathematics. 

“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,” said Prasad Tetali, Alexander M. Knaster Professor and department head of Mathematical Sciences at Carnegie Mellon, who is part of the team that submitted the proposal to the NSF.

man wearing eyeglasses showing something on a whiteboard
Prasad Tetali

“Mathematical reasoning is foundational to many branches of science and engineering. When human insight and ingenuity are paired with machine-assisted formal reasoning, the scope of the outcome is limitless,” Tetali said. “The beauty of investment in foundational work is that the long-term impact is difficult to predict and often far more rewarding than originally targeted or imagined. I see great potential for breakthroughs in multiple mathematical research areas.”

The three-year pilot institute based at CMU will bring together researchers from the Mellon College of Science — including Irina Gheorghiciuc and Michael Young – with the School of Computer Science’s Marijn Heule and Sean Welleck, in collaboration with researchers at the University of South Carolina and Georgia Gwinnett College. 

In its announcement, the NSF said the institutes will continue to empower researchers to explore new areas of mathematics. 

“The decision to launch this institute is a strong vote of confidence in its mission,” Avigad said. “We are humbled by that trust, and we will do everything we can to make good on it.”