Jul 09, 2026
Artificial intelligence is transforming one of the oldest disciplines: mathematics.
From generating proofs to verifying complex theorems, new AI-driven tools are changing how mathematicians work, collaborate and even define knowledge itself. At Carnegie Mellon University, a group of researchers is helping lead that transformation by bringing together logic, machine learning and automated reasoning.At the center of that effort is Jeremy Avigad, a professor in the Dietrich College of Humanities and Social Sciences’ Department of Philosophy and the Mellon College of Science’s Department of Mathematical Sciences, whose work in formalized mathematics is reshaping how proofs are written, checked and shared.“This is an exciting time for mathematics, as new technologies offer opportunities for exploration and discovery,” Avigad said.Carnegie Mellon’s strength lies not just in any one approach, but in the intersection of three: interactive theorem proving, neural AI and automated reasoning. Together, these areas form the foundation of a broader effort connected to the National Science Foundation-funded Institute for Computation and AI for Research in Mathematics (ICARM), which aims to advance AI methods for mathematical discovery and collaboration.Building a New Mathematical Infrastructure
