ProofPeer: Collaborative Theorem Proving

In today's computerised and scientific era, making our claims indefeasible is more critical and more relevant than ever. We need to make indefeasible claims about the stability of mission critical hardware and software components, e.g. about technology used in medicine where mistakes can be deadly, or about the security of computer systems in times where computer viruses are used as weapons of warfare.

In response to the challenge of making indefeasible claims, the fields of automated and interactive theorem proving have emerged. Automated theorem proving (ATP) is the mechanical checking of computerised proofs by mostly black box software components. Interactive theorem proving (ITP) builds on this by allowing human insight to guide and coordinate ATP systems in almost arbitrary ways. Interactive theorem proving has had noteworthy successes like the mechanisation of the proof of the four-colour theorem,
or the proof of the correctness of the seL4 operating system microkernel. These two examples show that verification problems in very different domains like pure mathematics and system level software can be successfully solved using the same technology, interactive theorem proving.

We believe that the time has come to reach even further and to be even more ambitious about the size of verification projects we are trying to tackle. But to be able to do so, we need a paradigm shift. The Linux operating system kernel consists of fifteen million lines of C program source code which has been contributed by over 1300 developers and over 200 companies. The verification of this kernel is completely out of reach for current ITP technology by several orders of magnitude.

While we manage to develop software at scale, it is as yet unknown how to do verification at scale. We therefore propose to expand the capabilities of ITP by creating collaborative theorem proving (CTP). We shall take the lessons and technologies of interactive theorem proving and integrate the lessons and technologies of the social web, in particular: 1) commons-based peer production and crowd-sourcing, 2) reputation systems, and 3) recommender systems. Sites like Wikipedia, Stack Overflow and Math Overflow have proven that these three components of the social web can result in unprecedented collaborative productivity. The focus of our research will be how to harness this productivity for the purpose of interactive theorem proving, establishing collaborative theorem proving as the social machine of ITP.

To this end, we will grow a online community called ProofPeer, which will be centrally hosted at http://proofpeer.net. After an initial phase of research and implementation, anyone will be able to become a proof peer and participate in this experiment of collaborative theorem proving.

The main goal of our research on collaborative theorem proving is to scale interactive theorem proving such that it becomes possible to tackle much larger verification projects than currently possible. A further goal is to popularise collaborative theorem proving so that a wider audience is equipped with the tools for making indefeasible claims.
The medium and long-term beneficiaries of this research will therefore be parties who either have a stake in making certain claims indefeasible, or who benefit from the educational effect of collaborative theorem proving. This includes the private sector, students at University of Edinburgh, and UK citizens in general.

A critical basis for the success of our research will be to grow a community of peers we can experiment on. At the same time, a large community of peers would constitute substantial impact all by itself because these peers will have been familiarised with collaborative theorem proving and could spread this concept further. We intend to grow a community of peers in various ways, via teaching, student projects, a Ph.D. student fully funded by the University, the publicly accessible ProofPeer webpage, a proofathon, a University-sponsored video that explains our research in a nutshell, and via publications, seminars, and industry talks. We think that our association with the Flyspeck project will lead to increased visibility of ProofPeer and collaborative theorem proving especially among mathematicians.

We also hope that our study of collaborative theorem proving will lead to commercialisation opportunities in the form of a startup/spinoff. The University of Edinburgh holds the UK record for number of spinoff companies, and we aim to tap into this experience via Informatics Ventures, the local commercialisation team.