ProofPeer – Collaborative Theorem Proving

Re:ProofPeer – Collaborative Theorem Proving by drewhk on Saturday November 30, 2013 @06:47AM (#6822907)

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

[ Parent | on HN ]

Re:ProofPeer – Collaborative Theorem Proving by auggierose on Saturday November 30, 2013 @07:30AM (#6822961)

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 [email protected], or just follow us on Github.

[ Parent | on HN ]

Re:ProofPeer – Collaborative Theorem Proving by drewhk on Saturday November 30, 2013 @07:01AM (#6822924)

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.

[ Parent | on HN ]