[bronty]

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.

[pirapira]

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

[tel]

Is that something a grep couldn't fix?

[bronty]

Yes, a grep could locate that.

[tel]

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.

[bronty]

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