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.
NSF Support
The institute is supported by U.S. National Science Foundation Grant DMS 2425401. The views expressed on these pages do not necessarily reflect those of the NSF.
If any ICARM meetings, resources, or innovation engineers are helpful to you, please indicate that in associated publications with a brief acknowledgment, such as the following:
- “Part of this work has been carried out at the Institute for Computer-Aided Reasoning in Mathematics (ICARM), which is supported by NSF Grant DMS 2425401.”
- “This work made use of …, maintained by the Institute for Computer-Aided Reasoning in Mathematics (ICARM) under NSF Grant DMS 2425401.”
- “We are grateful to the Institute for Computer-Aided Reasoning in Mathematics (ICARM) for technical support provided under NSF Grant DMS 2425401.”
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.
History
ICARM was conceived in 2023 as a response to challenges raised in workshops and a report issued 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.
You can find detailed descriptions of our activities in our annual reports:
Governance
The Institute and its leadership are advised by a Scientific Advisory Board, a Strategic Advisory Board, and an Educational Advisory Board, and overseen by a University Oversight Board. Information about our governance is available online; the members of the boards are found under People.
Visiting ICARM
ICARM is housed in the Robert Mehrabian Collaborative Innovation Center at 4720 Forbes Avenue, Pittsburgh, PA 15213. For travel, hotel, and dining information, see our visitor information page or Carnegie Mellon's visitor page.