EPSRC Reference: 
EP/L011794/1 
Title: 
ProofPeer: Collaborative Theorem Proving 
Principal Investigator: 
Fleuriot, Dr J 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Sch of Informatics 
Organisation: 
University of Edinburgh 
Scheme: 
Standard Research 
Starts: 
01 April 2014 
Ends: 
31 March 2017 
Value (£): 
522,808

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
24 Oct 2013

EPSRC ICT Responsive Mode  Oct 2013

Announced


Summary on Grant Application Form 
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 fourcolour 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) commonsbased peer production and crowdsourcing, 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.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.ed.ac.uk 