‘Our modern society depends on correct mathematics’
Lack of proof verification can be fatal.
10 March 2019, the Ethiopian Airlines Boeing 737 Max crashed shortly after take-off from Addis Ababa, killing 157 people.
According to the BBC, the preliminary report by Ethiopia's Aircraft Accident Investigation Bureau suggested that, “the pilots were struggling to deal with an automated safety system”.
In order to check a data system for errors, engineers use specific tools.
‘For instance, at the frontline, technicians try to make sure that the system does not make
The researchers in the project Homotopy Type Theory and Univalent Foundations combine logic, computer science and mathematics, to try to find a language to express mathematics in a way a computer can understand. Data systems depend on these methods in order to check for errors, but Bezem and Dundas work at a more fundamental level.
‘We are in the rear making sure that the mathematical underpinnings, on which the engineers’ tools ultimately depend, are correct’, Dundas says.
‘This is just one example of how our modern society depends on correct mathematics’, Bezem says.
- Read other stories about the project here
As Bezem and Dundas invited world-leading scholars to work together on Homotopy Type Theory and Univalent Foundations at CAS, they made Oslo a temporary world capital in the field.
We asked the two project leaders how the year at CAS had been, as they are about to return to their home institutions where tutoring and other tasks await.
Time to try out ideas
What was the year at CAS like?
‘When I first arrived in Norway 20 years ago, I found Norwegian universities more “permissive” than the Dutch ones, but I think that is no longer the case. Research time is very fragmented. Therefore, CAS offers great conditions for doing research, because you don’t have the distractions of administrative duties, and we have our favourite colleagues around us’, Bezem says.
Dundas compares CAS to a sabbatical:
‘The difference is that at CAS, you gather a group that is interested in a common theme, and you work together as a team. Additionally, it is not so much that I am spared administrative duties and teaching, but the fact that the whole group is. That has definitely been fruitful.’
Bezem and Dundas say that one of the project’s main results this year would not have happened without people being in the same place and talking. Some of the project members have proved the Voevodsky’s Homotopy Canonicity Conjecture, named after the late IAS mathematician Vladimir Voevodsky, who died in 2017. Vladimir Voevodsky is one of the founders of Homotopy type theory, and had planned to join the project. The project leaders describe this as a “major breakthrough” in the field.
‘At CAS, you have time to play with an idea together. CAS gathers people together long enough to make discoveries. Essentially, the fellows who made the breakthrough used one of the tools lying around, but there was no particular reason why it should be exactly that tool, there was as little intuitive reason to use the pliers when the problem looks like a nail. This wouldn’t have happened if the right people weren’t gathered at the right time’, Dundas says.
A new framework for teaching mathematics
It is obvious that a researcher cannot stay at CAS forever.
‘To never teach or supervise my students again would be sad’, Dundas says, but confesses that he is returning to perhaps too much of a good thing.
‘I will teach first-year in calculus’, he said, laughing.
‘I will also teach the following semester’, Bezem comments, and says that one of the results of the CAS year will be a book for advanced undergraduate students.
‘I will lecture from this book in progress, which is efficient because then you find out what works, and what needs to be modified’.
The book is for undergraduates, but is based on the new framework in Univalent Foundations, which Dundas describes as “sort of like a new language”:
‘It is not that the content is more difficult, but both lecturers and students will tend to be unfamiliar with it because we are giving ordinary undergraduate curriculum in the new framework that we are working on. It is almost like introducing a group of Norwegian-speaking kindergarten kids to a new game, and explaining it in English. The game is not the most difficult thing here, nor the main goal, but the language is’.
The project received the first CAS Alumni Fellowship Grant, which enables Bezem and Dundas to continue working with the CAS fellows, and invite them to Bergen.
Bezem and Dundas describe CAS as an almost perfect setting for mathematical research.
‘We do not depend on a lab, open access is in practice almost achieved in mathematics. CAS offers the opportunity to gather the right people in ideal circumstances to do mathematics’, Dundas concludes.
Several fellows have already concluded their stay at CAS. Here's what some of them them had to say about their time at the Centre:
Emily Riehl, assistant professor at Johns Hopkins University
‘A major innovation in univalent foundations over the past few years has been the development of cubical type theory, and I had hoped to spend my time at CAS learning about the latest developments from the experts. But the outcome was much better: what began as naive questions about the current state of the art expanded to long daily discussions which have now borne fruit in a collaborative project, the results of which we'll present to our colleagues at the International Conference on Homotopy Type Theory later this summer.’
Peter Dybjer, professor at Chalmers University of Technology and University of Gothenburg ‘I am grateful for being a CAS fellow, and thus meeting an impressive group of leading senior and junior researchers in our field. What is special about CAS is that the group is limited to 8-9 people at a time. Consequently, personal friendships thrive, new collaborations are formed, and progress on important questions is being made. The conditions provided by CAS are the best: the beautiful premises, the helpful CAS staff, and the pleasantness of living in Oslo all contribute to the experience.’
Thierry Coquand, professor at Chalmers University of Technology, and University of Gothenburg The project is at the intersection of computer science (type theory) and mathematics (homotopy theory), and there is much to learn from each sides! The environment at CAS is relaxing and productive, and allows us to reflect and concentrate on the important questions of a field of research. Being here has given me a unique opportunity to collaborate with specialists in homotopy theory, and to learn more about this topic.
Steve Awodey, professor at Carnegie Mellon University, USA ‘When I planned my stay at CAS, I had a general goal: to understand "the connection between models of homotopy theory and models of type theory, specifically Quillen model structures and topos models of type theory”. I had a pretty specific project in mind to help me accomplish this goal. While I did (almost) finish the specific project, I ended up spending most of my time on a related project with two other CAS fellows, which developed while I was here. That project actually brought me a lot further toward my overall goal than the one that I had originally planned. It would not have been possible without the collaboration within the CAS group.’