10 Year Impact Statement
The IAS Special Year on Univalent Foundations of Mathematics, 2012-13.
The Special Year on Univalent Foundations was the Big Bang for the new field now known as Homotopy Type Theory and Univalent Foundations.
Through this program, the 25-30 researchers and students involved (and the 25 visitors who were there over the course of the year) were formed into a cohesive community of scientific colleagues. Starting from various different backgrounds, specializations, and even different disciplines (mathematics, logic, computer science), they emerged with a shared set of theoretical tools, a common working language, and a sense of community that has endured and carried them forward for the 10 years since then. The common focus of developing a new foundational system for mathematics that would be well-suited to computer formalizations, and yet convenient for everyday mathematicians to use, has led to theoretical and practical advances in mathematics, logic, and computer science, resulting in hundreds of research papers and public lectures (and probably millions of lines of code), scores of dissertations, several professorships, high-profile research grants, and regular international conferences, all focused on this new and vibrant field of scientific research at the intersection of several disciplines.
A textbook written as a collaborative project by the participants during the special year was self-published and made available at cost, and has been downloaded or purchased many thousands of times [1]. An international conference and summer school held after 5 years was attended by well over 100 students and researchers, and a second summer school held online during the Covid-19 pandemic had over 750 registered participants.
In addition to these practical indications of a successful scientific community, theoretical advances have been made toward the solutions of problems formulated during the special year. Several such important open problems were identified by the end of the year, and have guided research efforts since then. Two of these were recently solved by special year alumni: a team led by Special Year co-organizer Thierry Coquand (Gothenburg, Sweden) resolved a central conjecture formulated by IAS faculty member and co-organizer Vladimir Voevodsky on the computational tractability of the new Univalence Axiom; and Special Year participant Michael Shulman (University of San Diego) established a fundamental result conjectured by co-organizer Steve Awodey (Carnegie Mellon) on the mathematical applications of the formal system. And other participants, and their students, continue to advance the field with new computational tools and mathematical results.