DOD Grant to Reshape Foundations of Math

Steve Awodey (Carnegie Mellon University) has received a $7.5 million, five-year grant from the Department of Defense (DOD) to reshape the foundations of mathematics by developing a new approach that allows for large-scale formalization and computer verification.

The grant, part of the highly competitive Multidisciplinary University Research Initiative program, will allow Awodey 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.

According to Carnegie Mellon's press release, homotopy type theory

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.

Read more.