I wonder how does this compare to the GitHub + package manager combo. Using these tools, platforms like Ruby or Node.js became massively collaborative. To me proof development is similar to software development, so it should work as well. By the way, Coq will soon get a package manager based on OPAM: http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20131126?...
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. :-)
Cool project! This is a really promising area of research.
Our group at Stanford recently published some early work that shows how a different kind of large-scale collaboration, via MOOCs, can be combined with theorem provers towards pedagogical ends. http://hci.stanford.edu/publications/paper.php?id=260
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 started working on a very similar idea half a year ago -- with machine learning and everything (my domain was proofgraph.org). I had to suspend it since it is larger than a one mans freetime project. I am very glad that someone started with a similar idea!
Will it be open source? I would be happy to contribute (I work full-time with Scala).
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.
I wonder how does this compare to the GitHub + package manager combo. Using these tools, platforms like Ruby or Node.js became massively collaborative. To me proof development is similar to software development, so it should work as well. By the way, Coq will soon get a package manager based on OPAM: http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20131126?...