Mission
Several new technologies are becoming available to support mathematical reasoning and discovery. These include:
- interactive theorem proving and formalization,
- automated reasoning and symbolic AI, and
- machine learning and neural AI.
The Institute for Computer-Aided Reasoning in Mathematics is one of seven NSF mathematical science research institutes. Its mission is to
- empower mathematicians to take advantage of new technologies for mathematical reasoning and keep mathematics central to everything we do;
- unite mathematicians of all kinds, computer scientists, students, and researchers to achieve that goal; and
- ensure that mathematics and the new technologies are accessible to everyone.
In the age of AI, mathematics is more important than ever, enabling us to pose precise queries, write exact specifications, ask for explanations, demand justification that we can audit independently, and develop symbolic models we can reason about and explore.
History
ICARM was conceived in 2023 as a response to challenges raised in workshop and report issues by the National Academies of Sciences, Engineering, and Medicine, titled Artificial Intelligence to Assist Mathematical Reasoning. Funding was announced on August 4, 2025 and the institute was launched as a three-year pilot on September 1, 2025.
Carnegie Mellon University
The institute is located on the campus of Carnegie Mellon University, which provides administrative oversight and infrastructure. We are supported by the Mellon College of Science, the School of Computer Science, and the Dietrich College of Humanities and Social Sciences.
Support
The institute is supported by U.S. National Science Foundation Grant DMS2425401. The views expressed on these pages do not necessarily reflect those of the NSF.
