Formalisation in Theory and Practice

Professor Peter Aczel

Mathematicians have known for a long time that in principle it is possible to formalise mathematics so that proofs could be checked by a computer. Nevertheless, until fairly recently, complete formalisation has almost never been undertaken. The process would have been very tedious and time consuming and the result would have been too unreadable by a human.

In recent years the rapid progress in the power and design of computer systems has generated new systems that can not only check the correctness of formalised proofs, but can be used interactively to help in the preparation of the formalised mathematics. By using these systems some of the more routine details of formalisation can be left to the computer.

The main motivation for the development of these computer systems has come from Software Engineering, where it has been felt that software systems, particularly critical ones such as those used in controlling the safety of nuclear power stations, should be proved to meet explicit formal specifications, and moreover that the proofs should be formalised and checked by computer. Apart from this motivation there is the promise of computer systems which will be of genuine assistance to pure mathematicians in the creation of proofs of theorems. Such systems could also incorporate features of computer algebra systems which are already available.

However, much theoretical and experimental work is still needed. Deeper understanding of the logical frameworks that are being used for formalisation, and the development of new mathematical abstractions to make formalisation more practical, are needed. More work needs to be done on the creation and use of large scale libraries of formalised mathematics. The ideal background for this kind of work would be a combination of computer science and mathematical logic with certain areas of algebra such as category theory.

In Manchester work has been under way on this topic, jointly with the Computer Science Department.