New theories for computer verification

Axel Ljungström will receive his doctoral degree in mathematics from Stockholm University in 2025. Thanks to a grant from the Knut and Alice Wallenberg Foundation, he will hold a postdoctoral position with Professor Ulrik Buchholtz, University of Nottingham, United Kingdom.

The more sophisticated mathematics becomes, the more difficult it is to find errors in mathematical proofs. One way to make proofs more reliable is to verify them using a computation software called a proof assistant. The project aims to develop theories that are the foundation for modern proof assistants. A particular focus is the use of proof assistants for doing homotopy theory, which is a part of algebraic topology.

For a computer to understand the abstract definitions of homotopy theory, a new language is required. Currently, many proof assistants are based on type theories, a collection of logical systems developed to form the basis of all mathematics. One of the most important modern type theories was invented in the 1970s by Per Martin-Löf, now professor emeritus of logic at Stockholm University. Eventually, a whole new mathematical system has emerged – homotopy type theory (HoTT). This is tailored for the computer verification of proofs in homotopy theory. 

Homotopy type theory is a mathematical system with its own rules. Often, new mathematics must be invented to be able to express classical homotopy theory in other terms. Another step in the project is to then investigate whether algorithms can be used for conducting computer verification. In this way, proofs can be drastically simplified, even for mathematical theorems that do not appear to be computational in nature. 

Photo: Elias Tingström