ProofPeer – Collaborative Theorem Proving

While proof development shares A LOT of traits with software development, it is not the same. For example, proof development also shares A LOT of traits with writing an academic paper. I think Github + package manager is definitely the baseline to beat, but I believe something much better is possible when focusing on the particular case of a collaborative theorem proving system. It might even turn out that this particular case is not that particular at all. :-)

Very interesting work, I just looked at your paper. I like the idea of the proof cache which improves the individual user experience exploiting the collaborative setting; although I am not sure how this could be generalized to more general automation than the kind of term rewriting based search you describe.

Did you grade student derivations in a binary fashion, i.e. correct / incorrect, or did you also take into account especially "pretty" derivations or something like that?

I really love the "Informal Reasoning" support idea. Does it have a reputation system (I see it on the architecture diagram)?

In my proofgraph I used the notion "certificate". Theorems are either certified by proof (strongest one, multiple proofs are possible) or are signed by third parties (committee, reviewers, trusted experts, or semi-formal automatized systems or programs like Mathematica or Sage) or self-signed (weakest).

EDIT: Ah, I see, there is a separate page explaining that.

Yes, it will be open-source, and we will host it at https://github.com/proofpeer .

We will start coding full-time on it around February 2014.

If you want to collaborate, send an email to contact@proofpeer.net, or just follow us on Github.

Yep, Edinburgh rocks. ;-)