Here, the fellows of the CAS project Homotopy Type Theory and Univalent Foundations will present themselves and their work, as well as discuss the plans and goals for their research stay at CAS Oslo. 

About the project:

What is a proof? And what does it mean to be equal?

The answers to these questions vary enormously, both through time, but also from one culture to another. The modern mathematical proof may seem the most rigorous of all alternatives. Still, the ideal of well-documented, accountable knowledge, communicated with a proof certificate, is in no way reached. Typically, the validity of extremely complicated mathematical proofs is still supported only by the community's trust in peer review performed by a few acknowledged experts.

Since the modern society depends on mathematics, secure foundations are important. In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power, and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge. 

In this approach equality has a topological interpretation, yielding great flexibility. Our project aims at further exploring this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.


Problems viewing the registration form? Please register here.