Proof Market: Submit Coq proof, get paid with Bitcoin

by waffle_ss • 13 years ago

92 30 13 years ago

elwell• 13 years ago

This sort of 'market' could surely be used for many other use-cases.

bronty4• 13 years ago

It actually can't -- a fundamental characteristic of this marketplace is that the work can be automatically verified [1].

As part of my PhD work, I created a service for crowdsourcing the verification of Java programs which relied on the same characteristic: http://homes.cs.washington.edu/~mernst/pubs/veriweb-oopsla20....

One limitation of these crowd-sourcing approaches is that, in practice, validation ("are we trying to build/prove the right thing?") is as important, if not more important, than verification.

[1] this might not be quite true yet, since a solution of "admitted." would pass the Coq checker.

tel3• 13 years ago

Is that something a grep couldn't fix?

pirapira6• 13 years ago

"admit" does not pass the checker right now. coqchk -o is used to detect those assumptions.

milohoffman• 13 years ago

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

Bakkot• 13 years ago

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.

gwern• 13 years ago

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 market never takes off - as is one's default expectation - it'd not be pleasant for buyers to have paid up front.

pirapira6• 13 years ago

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

bronty4• 13 years ago

It depends on whether or not the buyer allows for proof irrelevance.

There are cases where _human_ buyers care about the structure of the proof. In particular, just like with code, you'd prefer a proof that is maintainable, modular, and not-too-hard to update if your assumptions or claim changes.

bevan• 13 years ago

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.

agravier• 13 years ago

About bountify.co, Why does it request profile write permissions when OAuthing wit github? It puts me off.

djhworld• 13 years ago

I like the idea, however it appears as if the buyer has to wait until the seller has done the work before sending them payment.

How much confidence could the seller (i.e. the person doing the proof) have about the buyers ability to pay before they embark on completing the work?

A much better approach would be the buyer puts up the problem they want a proof for and then pays an escrow service, that way you can have more confidence that payment will be completed.

yetanotherphd• 13 years ago

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.

equivrel• 13 years ago

You probably mean homomorphic encryption[1].

[1] https://en.wikipedia.org/wiki/Homomorphic_encryption

paulgb• 13 years ago

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.

pirapira6• 13 years ago

I wonder which is easier to encode, natural deduction or Hilbert style.

velis_vel• 13 years ago

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.

AlexCoventry• 13 years ago

I don't know how to do that, but I did think about a cryptocurrency in which people got paid for optimizing objective functions.

https://docs.google.com/file/d/0B3qaT-ZL6aeKOHNEQWdpZEtRYWc/...

kordless• 13 years ago

Escrow implementation details aside, I love the idea of paying for information with a system that provides a method for communicating information securely between two parties. One of the more overlooked features of Bitcoin allows for message signing: http://bitcoin.stackexchange.com/questions/3337/what-are-the...

With a signing method, you can simultaneously prove someone created information containing a solution to a problem and the fact someone else paid them for the information.

platypii• 13 years ago

This seems like a cool idea. What I like about it is the way that it assigns a quantifiable value to mathematical proofs, and incentives their production.

Assuming proofs are valuable (which I believe they are), then by creating a market we can learn an approximation of what they are really worth to people.

Also I like that it is another outlet for mathematicians to profit from their skills. The options for pure math as a career are fairly bleek right now (fuck the nsa, academia maybe, not many research jobs in industry). I could see this market as a way to incentive more pure math research.

tel3• 13 years ago

I don't know if Coq with nested universes is known to be inconsistent yet, but I suppose that for this to work someone must always bankroll `inconsistent : forall a : Set, a` at something significantly higher than any other proof on the market and the system should reject repeated proofs.

markeightfold• 13 years ago

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 escrow model is implemented, you can actually imagine the mathematical proof market maker acting like a bank, loaning out or otherwise investing bitcoins while the world waits for a verified proof; say, of the abc conjecture [6a] or the goldbach conjecture [6b]. This might be one small way to disrupt Wall St [7a], [7b]. In particular, such a market, when more highly developed, provides skilled mathematicians and scientists incentives to work on math and ( computer ) science problems in an open source format that benefits everyone - since everyone can look at and learn from their proofs - rather than quantitative trading in a closed format that actually causes long term social harm and political instability [IMHO]. I am thinking here of Goldman Sachs and Renaissance Technology founded by James Simons. Imagine if an incentive structure existed that encouraged all these smart folks to work on what is essentially verifiable open source software [8].

[1] http://www.cs.princeton.edu/courses/archive/fall09/cos441/in... [2] http://blogs.scientificamerican.com/guest-blog/2013/10/01/vo... [3] http://www.heidelberg-laureate-forum.org/event_2013/ [4] http://homotopytypetheory.org/book/ [5] http://www.michaelnielsen.org/ddi/how-the-bitcoin-protocol-a... [6a] http://www.nytimes.com/2012/09/18/science/possible-breakthro... [6b] http://xkcd.com/1310/ [7a] http://cdixon.org/2013/12/31/why-im-interested-in-bitcoin/ [7b] http://cdixon.org/2010/01/23/how-to-disrupt-wall-street/ [8] This is a pipe dream.

pirapira6• 13 years ago

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.

shinobu• 13 years ago

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.

[1] https://en.wikipedia.org/wiki/Overjustification_effect

pirapira6• 13 years ago

There is a similar site [1] without external incentives (actually Proof Market is based on this). This site has active audience posting problems and proofs. Possibly Proof Market ends up in another example of overjustification.

[1] http://as305.dyndns.org/aps/

Proof Market: Submit Coq proof, get paid with Bitcoin

Related Stories