Two central questions in the foundations of mathematics are: '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.