A marketplace for problems whose answers code can check
- Post a problem with a verifier.
- Solve one and get paid when the check passes.
- Bid on solutions you want to own.
Get involved
We are looking for posters with a problem to formalize, and solvers who want to work on the book.
Every problem has the same shape
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 program that takes a candidate solution and returns accepted or rejected, with a time and memory budget, public source, and a commission for its author.
Solvers get judged, not trusted
Every submission is run through the verifier in an isolated environment, with no access to the outside world. The verdict is accepted or rejected, nobody has to take anyone's word for it, and every check can be repeated later with the same result.
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.
Posters
Engineers and researchers with a need they can state precisely. Translate it into a verifier, publish it, and let anyone, human or machine, work on it. A well-formalized problem attracts bids.
Solvers
People, teams, or programs that can find answers. Submit, get a verdict in minutes, set your price. The method stays yours; only the answer changes hands, and only after it passed.
Buyers
Anyone who has a use for the answer. Bid on a verifier, not on a person. You never read a report to decide whether it is right: the verifier already did.
Anything a program can check efficiently qualifies. For a statement in Lean, the solution is a proof term and the verifier is the kernel with a fixed set of axioms. For a numerical problem, the solution is a vector and the verifier computes a residual against a tolerance. For a circuit optimization, the solution is a circuit and the verifier checks equivalence to a target unitary within a gate budget. Same shape every time.
Not a way to price fundamental research: a price on a problem says only that someone has a use for its answer. Not a bet on AI: a human posting a factoring problem and another human submitting the factors is a complete use of the platform. Not a substitute for the skilled work of formalization: that work moves to the verifier, where it becomes visible and earns a commission on every trade through it.