ProofPeer is a project to create a cloud-based social network interactive theorem proving system. I wrote about it a year ago. The project looked dormant since about July, but now it got funding and is accepting PhD studentship applications.
The goals of the project are very ambitious. The ProofPeer team is planning to build a massively collaborative theorem proving system that would be able to handle millions of users, tens of thousands concurrently, while being sound, extensible and relatively simple to use. I am really trying to restrain my sometimes excessive skepticism here, but come on: millions of people doing formal proofs? Like, who is going to force them to do that? Has formalized mathematics become cool recently and I haven’t noticed?
In my opinion (at least as far as far as formalized mathematics is concerned) there are two preconditions for attracting users to such system – a readable proof language and foundations based on some sort of set theory. Let’s talk about the readability. Of course readability is a very subjective term. However, people who may want to do formal proofs have been most likely trained in mathematics. They are used to proofs that look and can be read in a very specific way. This gives a good criterion for readability: a formal proof is readable if someone familiar with standard mathematical notation can look at it and have a good guess on what assertion is proven and why the assertion is true. Now, let’s look at an example proof written in ProofSript – the ProofPeer forrmal proof language:
proof REPEAT all_intro_tac REPEAT imp_intro_tac conj_intro_tac REPEAT assumption_tac end
This is nor readable, at least in the way I understand it.
The second condition is familiar foundations. In my opinion this is a bit less important than readable presentation of proofs, but still a foundation that is radically different from what mathematicians already know creates an additional barrier for new users. The ProofPeer site suggests that the foundation must contain HOL and should contain ZFC. The decision is to focus on one logic rather than create a generic system that is able to support many logics. The argument here is that supporting many logics would lead to fragmentation of community. I think this is a mistake. Supporting only one logic will probably lead to the situation that potential users who do not like say HOL, but prefer ZFC (like myself) will not become actual users.
Anyway, although I think chances of ProofPeer project reaching its goals are extremely small, I still think that a lot of good research may come out from it. If not exactly in formalized mathematics, then perhaps in formally verified software? As a programming language and a proof language ProofScript may become a better Coq.