ProofPeer

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.

Advertisements

Tags: , ,

3 Responses to “ProofPeer”

  1. Andreas Says:

    Hi, I just discovered your blog and this article.

    It appears to me that you often deal in your blog with the question, if it is possible to create a collaborative theorem proving system. In April 2014, I created the site http://www.bookofproofs.org, which is designed to be a collaborative system for mathematical proofs.

    In the mid term, I plan to extend this site by a formal language reflecting all proofs contained in it, for the time being, however, it seems for me to be more important to get any mathematicians involved in this collaborative initiative.

    I share your concerns that only a few people might really want to do formal proofs. With this concern in my mind, I’m trying to go with my site a mid-way between two extremes: a formal system, which is logically correct and precise, but not understandable to a broad community (and so cannot be collaborative by design) and a site consisting only informal articles about topics in mathematics (however cannot be by design formalized).

    My mid-way approach is to separate formal entries (like axioms, definitions, theorems and proofs) from entries containing other stuff (like explanations, applications and examples). Both types of content can co-exist on my site and are put into relation to each other.

    My hope is that this approach could be both: collaborative by attracting people containing informal, but still interesting stuff, and formalize mathematical proofs according to modern proving standards (or even be readable by a proving system).

    I’m looking forward to read your opinion on this approach.

  2. slawekk Says:

    Your site looks great. It is unclear for me however how you want to distinguish it from PlanetMat.org? It seems like a very similar idea and it has been in existence for a long time with a large community.
    I also think that mixing formal and informal text is the best approach, but I suspect that the word “formal” means something different for me than for you. For me a formal proof is one that is written in a formal proof language. Strictly speaking a formal proof language does not have to be machine verifiable. However, in practice having a computer implementation is how you know that your proof language can be called a formal proof language.
    I disagree with your phrase “formal system, which is logically correct and precise, but not understandable to a broad community”. Historically it was the case that formal proof languages were not readable without special training. This is not a necessity though. The dialect of Isar (the Isabelle’s proof language) that is used in IsarMathLib is close enough to human proofs that I believe any difficulties in reading it by a mathematician are purely psychological. And one can do better than that – Gowers and Ganesalingam’s work shows that you can create a presentation layer that creates proofs indistinguishable in practice from ones written by a human.
    I am really curious how bookofproofs.org will deal with typical problems – the quality of proofs (human review is very expensive), people endlessly discussing whether infinity exists or if in fact 0.999… = 1 and so on. PlanetMath is quite successful, but I can see that even they recently have a problem of what I call “unchecked overrepresentation of non-standard approaches”.

  3. Andreas Says:

    Thank you for visiting my site. To answer your question, what most distinguishes bookofproofs.org from planetmath.org is that it is not a wiki (i.e. it is not article-based). I know, what you mean by “unchecked overrepresentation of non-standard approaches”, a problem, which many math wikis face.
    There are a lot of ideas at bookofproofs.org to deal with this problem. One rather central is the unification of notation valid in the context of a mathematical branch (just try out different nodes in any branch http://www.bookofproofs.org/branches/notation.php). Another idea is a proposed top-down structure (might still might be changed in time by the community), while articles in wikis have the same level of detail (e.g. article about algebraic structures in general is the same level of detail as an article about a particular group). Third, while in all math wikis (I know of) people mix definitions, theorems, proofs, examples and historical notes and put them into one article, bookofproofs.org requires a separation of all these types of content. This is I think a crucial feature unique to my site. By being able to post different proofs/ examples/ explanations, etc. to the same theorem independently from each other (see e.g. http://www.bookofproofs.org/branches/infinite-number-of-primes/), my site enables the co-existence of many a different (maybe both, standard and non-standard) approaches, all a) subject to corrective edits and b) to voting of the community. This way, the site bookofproofs.org does not prescribe, what the standard approach is. It rather lets the community decide (by voting for the most interesting one).
    I visited http://isarmathlib.org/. It was new for me and I like the formal proving dialect it proposes. You are right – it is more readable than what I’ve seen so far. However, I’m asking myself what the motivation is. I found the following motivation on the project site http://www.nongnu.org/isarmathlib/ : “Because it is fun and a good exercise for your brain. Some people also believe that formalized mathematics can be useful.” If I used isarmath on bookofproofs, I would use it to enable users for navigating through the theory, but not to represent the mathematical proofs behind – I still believe that having explanatory examples and some prose text about unsolved problems and motivations of the maths behind is at least as important as proofs being machine verifiable.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: