Communications of the ACM
Carnegie Mellon Awarded $7.5 Million Grant To Reshape Mathematics
Steve Awodey's team will explore the computational foundation for mathematics.
Credit: Carnegie Mellon University
Carnegie Mellon University's Steve Awodey has received a $7.5 million, five-year grant from the U.S. Department of Defense to reshape the foundations of mathematics by developing a new approach that allows for large-scale formalization and computer verification. The award, part of the competitive Multidisciplinary University Research Initiative (MURI) program, is one of 24 issued this year totaling $167 million over five years.
The grant will allow Awodey, professor of philosophy in the Dietrich College of Humanities and Social Sciences, and his research team to continue building on his groundbreaking discovery in 2005 of "Homotopy Type Theory," a deep and surprising connection between abstract, mathematical geometry and computational logic. Awodey and his team spent the past year at the Institute for Advanced Study (IAS) in Princeton, where he and IAS professor of mathematics Vladimir Voevodsky organized a research program called Univalent Foundations, devoted to exploring the use of Homotopy Type Theory to provide new computational tools for mathematical research.
The MURI award, officially entitled "Homotopy Type Theory: Unified Foundations of Mathematics and Computation," is through the Air Force Office of Scientific Research. It will establish CMU as the international center of research in this new field, which uses a fusion of tools drawn from abstract mathematics, such as homotopy and category theory, and the powerful computational paradigms of type theory and program verification. The resulting new, computational foundation for mathematics is not only an important theoretical advance. It also promises to provide a useful practical tool for mathematicians and other scientists in the form of powerful computer systems that can automatically verify the correctness of large and complex mathematical proofs and organize and unify a large body of verified mathematical theory in a form that can be reused for other scientific purposes. Equally important is the promise of new applications in theoretical computer science through the use of abstract geometrical intuitions and methods.
"This support will maintain the great momentum we gathered last year at the IAS and focus it on the research group here at CMU," Awodey says. "Carnegie Mellon is a world leader in logic, computer science, and formal verification, so it makes perfect sense for us to take the lead in this new area."
In addition to Awodey and Voevodsky, the research team consists of CMU's Robert Harper, professor of computer science, and Jeremy Avigad, professor of philosophy and mathematical science; Wesleyan University's Daniel Licata; and Michael Shulman of the University of San Diego. The team also will collaborate with researchers at MIT and in Slovenia, Sweden, and the United Kingdom.
The MURI program supports research conducted by teams of investigators that intersect more than one traditional science and engineering discipline in order to accelerate research progress.
No entries found