Proof Market: Submit Coq proof, get paid with Bitcoin
proofmarket.org
proofmarket.org
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.
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.
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.
https://docs.google.com/file/d/0B3qaT-ZL6aeKOHNEQWdpZEtRYWc/...
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.
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.
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.
With Coq, you don't have a problem of unsoundness. The problem you have is that the difficulty / time it takes to write a proof is often very sensitive to how you've written your assumptions and formulated the claim. You'd likely want to add a mechanism to the marketplace to reward workers for suggesting ways to improve the problem formulation.
For my Java project, we were using ESC/Java2 under the hood which is unsound in a lot of ways. We definitely observed workers taking advantage of these (either intentionally or not).
Also, it is unclear how to fit formalization of huge projects like classification of simple groups or IUTech in "reward for a proof" approach.
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.