New tools for troubleshooters

Dr Anders Mörtberg will receive funding from Knut and Alice Wallenberg Foundation to recruit an international researcher for a postdoctoral position at the Department of Mathematics, Stockholm University.

As modern software and mathematical theories become increasingly complex, it is also becoming increasingly difficult to ensure that they are entirely free of bugs and errors. One method used to increase their reliability is the use of a proof assistant – a computer program that can verify that the code is bug-free. The aim of the proposed project is to develop theories to provide a foundation for modern proof assistants.

Proof assistants can also be used to verify complicated mathematical proofs. One example is the four-colour theorem conjectured in 1852; this states that all planar maps can be coloured using just four colours, so that no neighbouring countries have the same colour. This was proved in 1976 using more than 1,000 hours of computer calculations, which also needed to be reviewed. A formal confirmation was finally provided in 2005, when a proof assistant demonstrated that there were no bugs in the calculations. 

Many contemporary proof assistants are based on type theories, a collection of logical systems developed with the aim to provide a foundation for all mathematics. The first modern type theory was introduced in the 1970s by Per Martin-Löf, emeritus professor of logic at Stockholm University. Recently, the development of type theory has been inspired by its links to homotopy theory, which is part of the mathematical field of algebraic topology. A number of new ideas, axioms and methods have grown from the union of the two theories, to help in tackling questions of verification. The project’s objective is not only to work with theoretical models, but also to further develop existing proof assistants so that bugs in mathematical proofs and software can be better prevented.

Photo Kristoffer Sahlin