USD's Largest Research Grant: Enhancing Proof Assistants with Homotopy Type Theory
It may seem like math is always right because it follows strict rules, but how do we know for sure that there are no mistakes? That is where formal verification comes in. Formal verification is the process of using a computer program, called a proof assistant, to prove that a system, model or algorithm is correct.
A recent breakthrough in proof assistant technology comes from a connection between two complex fields: formal logic (the study of reasoning) and topology (the study of shape and space). This would be like taking a clay sculpture and re-molding it using the same material but creating a completely different shape. The same thing happens when code is transferred from one library (a collection of code) to another; the code stays true to its original material while altering its shape. This insight has led to the creation of automated algorithms known as Homotopy Type Theory, a theory that makes it easier for computers to understand and verify complicated mathematical ideas.
“When people first hear about this theory, they think, wow, topology and logic are both super-abstract, so when you put them together it must be even more impossible to understand. But actually there’s an amazing synergy that happens, and the combined theory becomes simpler and more accessible," explained University of San Diego’s Associate Professor of Mathematics Michael Shulman, PhD.
In 2021, a team led by Dr. Shulman received a $7.5 million grant from the Department of Defense for a five-year project to apply Homotopy Type Theory to proof assistants. As the largest research award in the university’s history, it funds collaborative research by USD faculty, students and four other universities nationwide. As a result, numerous papers have been published, software prototypes developed and more than a dozen USD mathematics students have been funded to contribute to the project.
"One of the most rewarding things about this project has been finding ways to make this research accessible to students,” Dr. Shulman said. “I’m so proud of all the students who have worked on this project and the effort that they’ve put into it; all their contributions have made a difference to the results.”
This research is advancing both mathematics and computer science by improving the accuracy and reliability of complex proofs and software systems– a development that could have significant technological and security benefits.
“My dream is to have this new formal system, implemented in a proof assistant, that gives both mathematicians and programmers easier access to powerful tools to create and verify their work,” explained Shulman. “Then one day all the proofs and programs in the world can be certified as correct and error-free.”
- By Laney Green