A marketplace for verifiable problems
As AI performs more of R&D, the human bottleneck shifts to choosing which problems to solve and to phrasing them as evaluators AI can be scored against. Whoever can express a problem as a good evaluator can hand it to solvers and verify the answer automatically.
FormalMarket is a marketplace for exactly those problems: each one ships with a verifier, every submitted solution is machine-checked in a sandbox, and a price can only be attached to a solution that already passed. Buyers bid on answers that code, not opinion, decides are valid.
A problem becomes an evaluator
A problem is admitted only when its answer is expensive to find but cheap to check. That asymmetry is what makes a verifier possible: a Python verify(solution, rng) with a time and memory budget, public source, and a commission for its author.
Solvers get judged, not trusted
Every submission runs in a gVisor sandbox with no network and no writable bytes. The verdict records the seed and image digest, so any run can be replayed.
Verify, then price
Only an accepted solution can be listed. Buyers bid on a named verifier for a term; a bid at or above an ask in the same book settles immediately, each buyer paying their own bid. Asks never run out: a solution sells many times.
Answers stay private
A solution is readable only by its solver and the buyers whose trades settled. That a verified solution exists, who holds it, and its price are public; the answer is not.