Professor of Mathematics Michael Shulman Awarded $960,000 Research Grant

University of San Diego’s Professor of Mathematics Michael Shulman, PhD, received a $960,000 grant from the Air Force Office of Scientific Research to develop improved computing systems for validating mathematical proofs. 

While closely related to his 2021 grant that encompassed a five-year project to apply homotopy type theory to proof assistants (a computer program used for formal verification), this newly awarded grant will focus on the development of proof assistants and specifically the formalization of higher category theory in them. Higher category theory is the mathematical study of structures and their higher dimensional relationships.

In an excerpt from his grant application, Shulman explained, “existing proof assistants are a better match for some areas of mathematics than for others, limiting their potential uptake by working mathematicians and scientists.” His work to advance the formalization of higher category theory in proof assistants will create structure and consistency. This will in turn expand their coverage, accuracy and usefulness to professionals.

“The goal of mathematics is to seek truth statements,” Professor and Department Chair of Mathematics, Satyan Devadoss, PhD, added. “What Mike and his team have been doing to formalize this process, using mathematics machinery of category theory, not only has deep implications across mathematics, but a direct impact for our students on how they learn mathematics in courses we offer at USD.”

With this funding, Shulman will be able to carry out student research, faculty work, collaborations with other institutions and the hiring of a postdoctoral researcher to work on proof assistant implementations.