Challenge of Computer Mathematics Seminars/Workshops

Abstract

One may wonder whether proofs verified by a computer are at all reliable. Indeed, many computer programs are faulty. It was emphasised by de Bruijn that in case of verification of formal proofs, there is an essential gain in reliability. Indeed a verifying program only needs to see whether in the putative proof the small number of logical rules are always observed. Although the proof may have the size of several Megabytes, the verifying program can be small. This program then can be inspected in the usual way by a mathematician or logician.If someone does not believe the statement that a proof has been verified, one can do independent checking by a trusted proof-checking program, e.g. by a Proof Assistant.

A Proof Assistant satisfying the possibility of independent checking by a small program is said to satisfy the "de Bruijn" criterion. And it is based on the idea that although, provability is undecidable, being a proof of a given statement is decidable. All of the known Proof Assistant systems were primarily motivated by computer science applications. Being able to prove algorithms and systems correct is at the moment the main driving force for the development of Proof Assistants.

All this has been made possible by the progress in the foundations of mathematics: One can formulate all thinkable mathematical concepts, algorithms and proofs in one language. This is not in spite of, but partialy based on the famous results of Goedel and Turing. In this way statements are about mathematical objects and algorithms, proofs show the correctness of statements and computations, and computations are dealing with objects and proofs. Interactive computer systems for a full integration of defining, computing and proving are based on this. The human defines concepts, constructs algorithms and provides proofs, while the machine checks that the definitions are well-formed and the proofs and computations are correct. Results formalised so far demonstrate the feasibility of the Computer Mathematics.