Proof Market

This is a proof market for the Coq proof assistant and Agda.

News

Now using coq8.4pl3, which is not known to be inconsistent.

Agda service launched.

A problem feed is available

How to get proofs done for bitcoins

  1. Create a new problem
  2. (optional) add bounty
  3. wait for somebody to solve the problem on recent entries
  4. pay the price in bitcoins (if the solver sets a strictly positive price)
  5. see the proof

How to get bitcoins for proving

  1. find a problem on the list of all problems
  2. (optional) contact possible payers
  3. solve the problem
  4. post your solution with an additional price and your bitcoin address
  5. get the bounty
  6. wait for further payments (your proof still remains secret until the price is paid to you)

FAQ

When I submit my solution, the site says Fail.
Have you changed Admitted into Qed? Have you specified a correct bitcoin address? Have you checked the box about the license if you agree? Doesn't your solution contain some banned keywords such as "Extract" "ML" "Path" "State" "external" "Load" "Declare"?
Is this site written in Coq?
No, in Haskell, an inconsistent type theory. Although every type is inhabited, but not all terms can be typed.
I want to ask a question about a problem whose author is unknown.
We discourage posting to mailing lists as a default address for an anonymous author. Try posting a revised problem.
What version of Coq is running?
The Coq Proof Assistant, version 8.4pl3 (January 2014), ssreflect 1.5rc1 and MathComp 1.5rc1.
Why has False been proved?
First time, the meaning of False was changed. Second time, it was proved in Coq 8.4pl2, an older version.
What version of Agda is running?
Agda version 2.3.2.2
What Coq commands are used to check the answer?
  1. Some keyword screening (like Cd).
  2. coqc Definitions.v (if the problem contains definitions)
  3. coqc Answer.v
  4. coqc -require Definitions Verify.v (if the problem contains definitions. Otherwise, "-require Definitions " is omitted.)
  5. coqchk Answer -o -norec
What Agda commands are used to check the answer?
  1. agda Definitions.agda (if the problem contains definitions)
  2. agda --safe Answer.agda
  3. agda Verifier.agda
What Coq commands are used to check the problem?
  1. Some keyword screening (like Cd).
  2. coqc Definitions.v (if the problem contains definitions)
  3. coqc Answer.v (this comes from "Answer Template")
  4. coqc -require Definitions Verify.v (if the problem contains definitions. Otherwise, "-require Definitions " is omitted.)
Whos runs this site?
Kazuhiko Sakaguchi
What is the difference between the bounty and the price?
Though anyone can pay the bounty and the price, and the one who submits a correct proof gets them,the timing of payments are different. The bounty is paid just after the submitted proof is verified. The proof is hidden until the price is paid to the prover.
I can't Require Import Definitions.
Compile using coqc Definitions.v to produce Definitions.vo
Why the proofs need not be signed?
The proof and the associated bitcoin address are sent in a single https request. We assume their integrity.
Why don't you use the bitcoin scripts to verify proofs
Not yet just because we have not figured out how.
Can I use "admit" in the proofs?
No, not in answers. In a problem in the Definitions section, you can.
About the bounty on False, it seems like you just threw away 0.999 BTC and no one will ever get them.
Somebody got it.
Can I use this for software development?
Yes.
Are all solutions public?
No. Some solutions are hidden until a price is paid. The price is specified when the solution is submitted. However, we require every submission to be licensed under Creative Commons Attribution 4.0 International License.
I want to prove something based on a huge library. Can I?
Contact the site owner. Maybe they can add the library on the server.
The money should be sent using a 2-of-3 transaction.
Agreed. Figuring out how to do this. If I can implement a proof checker using Bitcoin scripts, that would be the best.
How can I learn about Coq?
I recommend reading and typing in Software Foundations
How can I contribute?
  1. Solve a problem
  2. post a problem
  3. raise bounty

Contact: s1111365@coins.tsukuba.ac.jp or https://twitter.com/proofmarket
This is based on kik's Yesod-Anarchy-Proof-Server