This sort of 'market' could surely be used for many other use-cases.
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).