This is a bit ordinary, since it is fundamentally just an escrow service. What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
Bitcoin does have a (non-turing-complete) scripting language built in for ensuring that transactions meet arbitrary requirements. I wonder what subset of proofs could be verified in that environment.
I wonder which is easier to encode, natural deduction or Hilbert style.
This is a bit ordinary, since it is fundamentally just an escrow service. What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
I don't know how to do that, but I did think about a cryptocurrency in which people got paid for optimizing objective functions.
This sort of 'market' could surely be used for many other use-cases.
I'm working on a very similar market for software development, where reward is granted based on completion of a unit test. Check it out at www.codetract.com
This is a bit ordinary, since it is fundamentally just an escrow service. What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
Bitcoin does have a (non-turing-complete) scripting language built in for ensuring that transactions meet arbitrary requirements. I wonder what subset of proofs could be verified in that environment.
The language doesn't support loops; in terms of flow control, you get if statements and that's it. So probably not much of interest.
Hm. Seems like it would make more sense for 'buyers' to submit btc along with the problem, which the market could then hold in escrow and release as soon as a proof passing the verifier was submitted. No need to trust anyone but the escrow service, between btc and machine proofs.
I created a marketplace for small coding tasks where buyers pay upfront when they post a code bounty (bountify.co). In practice, the pay-upfront model has worked well- there have been no disputes after several hundred bounties, and about 90% of bounties have received working solutions. However, bountify's domain (coding tasks) is probably better suited to upfront payment than proofmarket's. It's easy for code buyers to estimate the difficulty / value to sellers of small coding tasks, so buyers are reasonably assured of getting a solution within the one-week time limit. It seems like proof buyers would have a harder time estimating the difficulty of creating a proof, and that they might therefore be dissuaded from posting btc up-front for fear of nobody furnishing a solution.
Depends on who you want to put the burden onto, the buyers or the sellers. If a buyer has to pay up front, especially with a marginal service like this, they're exposed to opportunity cost (maybe they were going to do something else with that money, although interest rates don't really exist for Bitcoin yet) and counterparty risk (why do you trust this website to hold onto your bitcoins and not be hacked?). If this m…
I can mix both approaches. The buyer and other people can stash up bounty, which the first prover gets. I have not implemented this lest "bitcoin stolen from Coq proof exchange".
Hm. Seems like it would make more sense for 'buyers' to submit btc along with the problem, which the market could then hold in escrow and release as soon as a proof passing the verifier was submitted. No need to trust anyone but the escrow service, between btc and machine proofs.
I created a marketplace for small coding tasks where buyers pay upfront when they post a code bounty (bountify.co). In practice, the pay-upfront model has worked well- there have been no disputes after several hundred bounties, and about 90% of bounties have received working solutions. However, bountify's domain (coding tasks) is probably better suited to upfront payment than proofmarket's. It's easy for code buyers…
About bountify.co, Why does it request profile write permissions when OAuthing wit github? It puts me off.
I can mix both approaches. The buyer and other people can stash up bounty, which the first prover gets. I have not implemented this lest "bitcoin stolen from Coq proof exchange".
Way to avoid arbitrary risks and complications!
I added risks and complications. A feature called "bounty" is now available. Anyone can add bounty for a problem. The sum goes to the next solver.
This is fascinating to me. A couple comments and links. Here is a course on proof theory that uses Coq [1]. It is actually the course that Vladimir Voevodsky took when he was trying to understand proof and type theory [2], [3]. While writing the midterm paper, he discovered homotopy type theory [4]. More details on the bitcoin scripting language can be found in the excellent blog post by Michael Nielsen[5]. If the es…
This gives very broad perspective. I want to cite this comment when I talk about the site. I have never thought about disrupting Wall St, but I do share your pipe dream.
This project might be harmful because of overjustification effect. [1]
If there was some site 15 years ago that offered payment for writing an article on a given subject, would the number of contributors to wikipedia and thus the number of articles drop?
Also, it is unclear how to fit formalization of huge projects like classification of simple groups or IUTech in "reward for a proof" approach.