Nice project!<p>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: <a href="http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20131126?action=AttachFile&do=get&target=slides-braibant.pdf" rel="nofollow">http://coq.inria.fr/cocorico/CoqDevelopment/CRGTCoq20131126?...</a>
Cool project! This is a really promising area of research.<p>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. <a href="http://hci.stanford.edu/publications/paper.php?id=260" rel="nofollow">http://hci.stanford.edu/publications/paper.php?id=260</a>
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!<p>Will it be open source? I would be happy to contribute (I work full-time with Scala).