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