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

Proof Market: Submit Coq proof, get paid with Bitcoin

proofmarket.org

Post reply on HN
Print view View original

11–20 of 31 posts

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#11

Post by bronty »

tel wrote: post #10
bronty wrote: post #9

Earlier quoted context omitted.

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 try…

Is that something a grep couldn't fix?

Yes, a grep could locate that.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#12

Post by platypii »

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.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#13

Post by tel »

bronty wrote: post #11
tel wrote: post #10

Earlier quoted context omitted.

Is that something a grep couldn't fix?

Yes, a grep could locate that.

It's more a question of if there are any other known inconsistencies in Coq that could be used to trivially generate proofs which are artificial under human scrutiny but OK by an automated proof market.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#14

Post by tel »

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.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#15

Post by bronty »

tel wrote: post #13
bronty wrote: post #11

Earlier quoted context omitted.

Yes, a grep could locate that.

It's more a question of if there are any other known inconsistencies in Coq that could be used to trivially generate proofs which are artificial under human scrutiny but OK by an automated proof market.

You'd run into a problem if you let workers introduce assumptions (since introducing a contradiction lets the worker prove anything).

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

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#16

Post by gwern »

Bakkot wrote: post #3

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.

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.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#17

Post by bronty »

Bakkot wrote: post #3

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.

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.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#18

Post by markeightfold »

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.

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#19

Post by pirapira »

gwern wrote: post #16
Bakkot wrote: post #3

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.

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

Re: Proof Market: Submit Coq proof, get paid with Bitcoin

#20

Post by pirapira »

bronty wrote: post #9
elwell wrote: post #2

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

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 try…

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