NSF backs new Carnegie Mellon institute to apply AI in mathematical research and problem solving

Carnegie Mellon will lead a new federally funded research institute aimed at helping mathematicians use AI and formal methods to improve reasoning across science, cybersecurity, and finance.

Photo credit: Carnegie Mellon University, Professor Jeremy Avigad

Carnegie Mellon University has been selected to host a new national mathematics institute focused on artificial intelligence-supported research and discovery.

Funded by the National Science Foundation (NSF), the primary U.S. government agency responsible for supporting fundamental research in science and engineering, the Institute for Computer-Aided Reasoning in Mathematics (ICARM) will support efforts to modernize mathematical reasoning and apply it to real-world challenges in science, security, and the economy.

One of six NSF-supported math institutes in the United States, with additional support from the Simons Foundation, ICARM is based at CMU and led by Professor Jeremy Avigad from the Department of Mathematical Sciences and the Department of Philosophy.

The three-year pilot will bring together researchers from CMU’s Mellon College of Science and School of Computer Science, in collaboration with faculty from the University of South Carolina and Georgia Gwinnett College.

Supporting real-world problem solving

The institute is being developed in response to the growing influence of AI and formal methods in modern mathematics. According to CMU, machine learning is now being used to identify subtle mathematical patterns, with applications in finance, health care, and cybersecurity.

“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,” says Avigad.

The project forms part of the university’s wider AI research strategy, which includes work on verifying software systems and modeling complex systems through computation.

Training and community engagement

ICARM will also support training through summer schools, workshops, and a conference series. These events will provide opportunities for the mathematics community to engage with tools that support machine-assisted formal reasoning.

Prasad Tetali, Alexander M. Knaster Professor and head of the Department of Mathematical Sciences at CMU, believes that the institute’s work could influence how mathematics is taught in the future.

“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,” says Tetali.

The team behind ICARM includes Irina Gheorghiciuc and Michael Young from the Mellon College of Science, and Marijn Heule and Sean Welleck from the School of Computer Science.

Theresa Mayer, vice president for research at CMU, emphasized the timing of the initiative.

“Emerging technologies based on formal methods, AI and machine learning are transforming the landscape of mathematical research,” says Mayer. “We are grateful to the National Science Foundation for its leadership in establishing ICARM and recognizing the importance of this moment.”

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