Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

ProofPeer – Collaborative Theorem Proving

proofpeer.net

Post reply on HN
Print view View original

1–10 of 10 posts

Re: ProofPeer – Collaborative Theorem Proving

#2

Post by drewhk »

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).

Re: ProofPeer – Collaborative Theorem Proving

#3

Post by drewhk »

drewhk wrote: post #2

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.

Re: ProofPeer – Collaborative Theorem Proving

#4

Post by auggierose »

drewhk wrote: post #2

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).

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.

Re: ProofPeer – Collaborative Theorem Proving

#5

Post by clarus »

Nice project!

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?...

Re: ProofPeer – Collaborative Theorem Proving

#7

Post by unignorant »

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

Re: ProofPeer – Collaborative Theorem Proving

#8

Post by auggierose »

unignorant wrote: post #7

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?

Re: ProofPeer – Collaborative Theorem Proving

#10

Post by auggierose »

clarus wrote: post #5

Nice project! 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. :-)
Post reply on HN